GHC 8 + ImpredictiveTypes + $

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

GHC 8 + ImpredictiveTypes + $

Brendan Hay
Hi,

I have had a number of trivial compilation failures in many of my projects that contain instances for MonadBaseControl (from monad-control) since upgrading to GHC 8.

Now, I say 'trivial' since the actual fix is incredibly minor - a change of compose (.) to apply ($). What was less trivial was the (additional) hair loss arriving at the fix. I've put together a minimal example that demonstrates both the failing (pre-GHC8) and the fixed (GHC8) instances here:

Since I found the error message somewhat directionless, I'd like some help actually understanding the root cause and why the 'fix' works:

* I assume previously GHC did not fully check type aliases that were impredictive prior to GHC 8?

* What does this imply for a type alias such as for the alias RunInBase used in monad-control that contains RankNTypes:

* How does the use of ($) vs (.) fix this particular issue? (I'd naively assume the usage here would be equivalent.) I recall reading about ($)'s magical type alias somewhere - is this related?


Cheers,
Brendan



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GHC 8 + ImpredictiveTypes + $

Niklas Hambüchen
> Now, I say 'trivial' since the actual fix is incredibly minor - a change
> of compose (.) to apply ($). What was less trivial was the (additional)
> hair loss arriving at the fix

Tell me about it - when experimentally making a larger project work with
GHC 8, I spent a lot of time trying to understand the problem and was
rather disappointed that the climax of this effort was to replace `a = f
. g` by `a x = f (g x)` in two places.

The 8.0 migration guide
https://ghc.haskell.org/trac/ghc/wiki/Migration/8.0 already has a
section about "Impredicative types brokenness" - I would have
appreciated if it contained the simple sentence "In many cases, this can
be fixed by rewriting `a = f . g` to `a x = f (g x)`."

Maybe somebody can add it.

> * I assume previously GHC did not fully check type aliases that were
> impredictive prior to GHC 8?

Yes,
https://ghc.haskell.org/trac/ghc/wiki/Migration/8.0#Requirementforimpredicativetypes:
"In previous versions of GHC, it was possible to hide an impredicative
type behind a type synonym, because GHC did not always expand type
synonyms when checking for impredicativity."

> * What does this imply for a type alias such as for the alias RunInBase
> used in monad-control that contains RankNTypes:
> http://hackage.haskell.org/package/monad-control-1.0.1.0/docs/Control-Monad-Trans-Control.html#t:RunInBase -
> Is such an alias not safe in some sense? (Was it never safe?)

I'll let others answer this one.

> * How does the use of ($) vs (.) fix this particular issue? (I'd naively
> assume the usage here would be equivalent.) I recall reading about ($)'s
> magical type alias somewhere - is this related?

This page (I'm not sure if you already knew it before asking the question)

  https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism

describes the difference between `test1 x = foo (bar x)` and `test2 =
foo . bar`; it also has a "Special case for ($)" section which I believe
is the answer to your question. The summary is:

  " But Haskell programmers use ($) so much, to avoid writing
parentheses, that GHC's type inference has an ad-hoc special case for
($) that allows it to do type inference for (e1 $ e2), even when
impredicative polymorphism is needed. "

Niklas
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GHC 8 + ImpredictiveTypes + $

Adam Gundry-2
On 10/06/16 10:23, Niklas Hambüchen wrote:

>> Now, I say 'trivial' since the actual fix is incredibly minor - a change
>> of compose (.) to apply ($). What was less trivial was the (additional)
>> hair loss arriving at the fix
>
> Tell me about it - when experimentally making a larger project work with
> GHC 8, I spent a lot of time trying to understand the problem and was
> rather disappointed that the climax of this effort was to replace `a = f
> . g` by `a x = f (g x)` in two places.
>
> The 8.0 migration guide
> https://ghc.haskell.org/trac/ghc/wiki/Migration/8.0 already has a
> section about "Impredicative types brokenness" - I would have
> appreciated if it contained the simple sentence "In many cases, this can
> be fixed by rewriting `a = f . g` to `a x = f (g x)`."
>
> Maybe somebody can add it.

I've done so. Thanks for the suggestion!


>> * I assume previously GHC did not fully check type aliases that were
>> impredictive prior to GHC 8?
>
> Yes,
> https://ghc.haskell.org/trac/ghc/wiki/Migration/8.0#Requirementforimpredicativetypes:
> "In previous versions of GHC, it was possible to hide an impredicative
> type behind a type synonym, because GHC did not always expand type
> synonyms when checking for impredicativity."
>
>> * What does this imply for a type alias such as for the alias RunInBase
>> used in monad-control that contains RankNTypes:
>> http://hackage.haskell.org/package/monad-control-1.0.1.0/docs/Control-Monad-Trans-Control.html#t:RunInBase -
>> Is such an alias not safe in some sense? (Was it never safe?)
>
> I'll let others answer this one.

The required extensions will depend on the use site. If RunInBase is
used at the top level, no extensions should be needed. If it is used on
the left-hand side of an arrow, RankNTypes will be required. If it is
used as an argument to a type constructor (e.g. Maybe (RunInBase m b))
then ImpredicativeTypes will be required. For example:

    foo :: RunInBase m b          -- rank-1
    bar :: RunInBase m b -> Bool  -- rank-2, needs RankNTypes
    baz :: Maybe (RunInBase m b)  -- needs ImpredicativeTypes

Previous versions of GHC may have accepted the third case without
requiring ImpredicativeTypes in some circumstances, but this was a bug
that made typechecking unpredictably dependent on when type synonyms get
expanded (https://ghc.haskell.org/trac/ghc/ticket/10194).

In general, RankNTypes is fairly safe in that its typing rules are
fairly stable and well-understood. ImpredicativeTypes, on the other
hand, is basically broken and should be avoided as far as possible.

Hope this helps,

Adam

--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GHC 8 + ImpredictiveTypes + $

Brendan Hay
Thank you both!

On 10 June 2016 at 12:03, Adam Gundry <[hidden email]> wrote:
On 10/06/16 10:23, Niklas Hambüchen wrote:
>> Now, I say 'trivial' since the actual fix is incredibly minor - a change
>> of compose (.) to apply ($). What was less trivial was the (additional)
>> hair loss arriving at the fix
>
> Tell me about it - when experimentally making a larger project work with
> GHC 8, I spent a lot of time trying to understand the problem and was
> rather disappointed that the climax of this effort was to replace `a = f
> . g` by `a x = f (g x)` in two places.
>
> The 8.0 migration guide
> https://ghc.haskell.org/trac/ghc/wiki/Migration/8.0 already has a
> section about "Impredicative types brokenness" - I would have
> appreciated if it contained the simple sentence "In many cases, this can
> be fixed by rewriting `a = f . g` to `a x = f (g x)`."
>
> Maybe somebody can add it.

I've done so. Thanks for the suggestion!


>> * I assume previously GHC did not fully check type aliases that were
>> impredictive prior to GHC 8?
>
> Yes,
> https://ghc.haskell.org/trac/ghc/wiki/Migration/8.0#Requirementforimpredicativetypes:
> "In previous versions of GHC, it was possible to hide an impredicative
> type behind a type synonym, because GHC did not always expand type
> synonyms when checking for impredicativity."
>
>> * What does this imply for a type alias such as for the alias RunInBase
>> used in monad-control that contains RankNTypes:
>> http://hackage.haskell.org/package/monad-control-1.0.1.0/docs/Control-Monad-Trans-Control.html#t:RunInBase -
>> Is such an alias not safe in some sense? (Was it never safe?)
>
> I'll let others answer this one.

The required extensions will depend on the use site. If RunInBase is
used at the top level, no extensions should be needed. If it is used on
the left-hand side of an arrow, RankNTypes will be required. If it is
used as an argument to a type constructor (e.g. Maybe (RunInBase m b))
then ImpredicativeTypes will be required. For example:

    foo :: RunInBase m b          -- rank-1
    bar :: RunInBase m b -> Bool  -- rank-2, needs RankNTypes
    baz :: Maybe (RunInBase m b)  -- needs ImpredicativeTypes

Previous versions of GHC may have accepted the third case without
requiring ImpredicativeTypes in some circumstances, but this was a bug
that made typechecking unpredictably dependent on when type synonyms get
expanded (https://ghc.haskell.org/trac/ghc/ticket/10194).

In general, RankNTypes is fairly safe in that its typing rules are
fairly stable and well-understood. ImpredicativeTypes, on the other
hand, is basically broken and should be avoided as far as possible.

Hope this helps,

Adam

--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GHC 8 + ImpredictiveTypes + $

Edward Z. Yang
In reply to this post by Brendan Hay
Excerpts from Brendan Hay's message of 2016-06-10 01:59:51 -0700:
> * How does the use of ($) vs (.) fix this particular issue? (I'd naively
> assume the usage here would be equivalent.) I recall reading about ($)'s
> magical type alias somewhere - is this related?

When you say f $ a, where a is a polymorphic variable, we need to
instantiate the type variables in ($) :: (a -> b) -> a -> b with
quantified types; i.e., do an impredicative instantiation.  GHC has
never been able to do this, so there's a hack for the typechecker
to treat 'f $ a' as if it were just 'f a' (no more impredicative
instantiation).

(.) is not special cased similarly, which is why it doesn't work.
I don't know if we could special case it to solve this problem.

Edward
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GHC 8 + ImpredictiveTypes + $

David Feuer

I'm pretty sure we *could*, but special case hacks in the type checker are horrible. So we shouldn't.

On Jun 10, 2016 11:13 AM, "Edward Z. Yang" <[hidden email]> wrote:
Excerpts from Brendan Hay's message of 2016-06-10 01:59:51 -0700:
> * How does the use of ($) vs (.) fix this particular issue? (I'd naively
> assume the usage here would be equivalent.) I recall reading about ($)'s
> magical type alias somewhere - is this related?

When you say f $ a, where a is a polymorphic variable, we need to
instantiate the type variables in ($) :: (a -> b) -> a -> b with
quantified types; i.e., do an impredicative instantiation.  GHC has
never been able to do this, so there's a hack for the typechecker
to treat 'f $ a' as if it were just 'f a' (no more impredicative
instantiation).

(.) is not special cased similarly, which is why it doesn't work.
I don't know if we could special case it to solve this problem.

Edward
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GHC 8 + ImpredictiveTypes + $

Edward Z. Yang
But I feel there ought to be a way to apply this hack systematically,
so that we can handle these cases, which are "easier" than full
impredicativity.  For example, as a dumb proposal, if we treated
($) and (.) as macros (inline before typechecking), that would
give us correct typechecking for both these cases.  So maybe
some sort of stratification would solve our problem.

Edward

Excerpts from David Feuer's message of 2016-06-10 08:21:31 -0700:

> I'm pretty sure we *could*, but special case hacks in the type checker are
> horrible. So we shouldn't.
> On Jun 10, 2016 11:13 AM, "Edward Z. Yang" <[hidden email]> wrote:
>
> > Excerpts from Brendan Hay's message of 2016-06-10 01:59:51 -0700:
> > > * How does the use of ($) vs (.) fix this particular issue? (I'd naively
> > > assume the usage here would be equivalent.) I recall reading about ($)'s
> > > magical type alias somewhere - is this related?
> >
> > When you say f $ a, where a is a polymorphic variable, we need to
> > instantiate the type variables in ($) :: (a -> b) -> a -> b with
> > quantified types; i.e., do an impredicative instantiation.  GHC has
> > never been able to do this, so there's a hack for the typechecker
> > to treat 'f $ a' as if it were just 'f a' (no more impredicative
> > instantiation).
> >
> > (.) is not special cased similarly, which is why it doesn't work.
> > I don't know if we could special case it to solve this problem.
> >
> > Edward
> > _______________________________________________
> > Haskell-Cafe mailing list
> > [hidden email]
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> >
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe