[Haskell-cafe] GHC 8 + ImpredictiveTypes + $

[Adam Gundry]

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/