[Haskell-cafe] GHC 8 + ImpredictiveTypes + $

[Brendan Hay]

Thank you both!

On 10 June 2016 at 12:03, Adam Gundry <adam at well-typed.com> 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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160610/ea250685/attachment.html>