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#Requirementforimpredicat...: "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-... - 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/

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" 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 Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe