[Haskell-cafe] Monomorphism restriction [Was: Rank2Types in let bindings]

[Brandon Allbery]

And just to complicate things more, there is also MonoLocalBinds
which monomorphizes certain let bindings and is turned on by some
extensions (iirc including type families) because they get much harder to
type otherwise.

On Thu, Oct 7, 2021 at 1:30 PM Olaf Klinke <olf at aatal-apotheke.de> wrote:

> >
> > {-# LANGUAGE RankNTypes #-}
> > > newtype General = General {
> > >     useGeneral :: forall a. Integral a => a -> Bool
> > >     }
> > >
> > > doesNotWork :: General
> > > doesNotWork = let
> > >          g = even :: forall a. Integral a => a -> Bool
> > >          b = specializeGeneral g
> > >          in General g
> > >
> > > doesWork :: General
> > > doesWork = let
> > >          g = General even
> > >          b = specializeGeneral (useGeneral g)
> > >          in g
> > >
> > > specializeGeneral :: (Int -> Bool) -> Bool
> > > specializeGeneral p = p 5
> > >
> > > I was under the impression that one can always use a more general type
> > > where a more special type is needed. In `doesNotWork` above, despite
> the
> > > explicit Rank-2 type annotation, usage in `specializeGeneral`
> apparently
> > > makes the compiler infer the type of `g` to be (Int -> Bool) and
> > > complains that `a` can not me matched with `Bool`. What gets me is
> that
> > > the compiler error is at `General g`, so the compiler must have
> ignored
> > > my Rank-2 type annotation. Should it be allowed to do that?
> > >
> > > Olaf
> >
> > Hi Olaf,
> >
> > This is the monomorphism restriction. g is a binding without a
> > signature, so it gets specialized. The type annotation is part of
> the
> > body of g, but if you want to generalize g it should be a separate
> > declaration
> >
> >      let g :: forall ...
> >          g = ...
> >
>
> Oh, thanks! I should have suspected. But somehow I feel my type
> annotation should have circumvented the monomorphism restriction. So
>    g = even
> is a pattern binding and therefore subject to monomorphism restriction,
> regardless of following type annotation?
>
> So thanks for teaching me that it is not irrelevant where to place a
> type annotation. To this day I believed that
>    name = expression :: type
> and
>   name :: type
>   name = expression
> are equivalent because one is syntactic sugar for the other. Do the two
> give rise to different elements in the abstract syntax tree? Am I the
> only one who finds this odd? Which Haskell book should I have read to
> be aware of this? The Consequences part in Section 4.5.5 of the Haskell
> report mentions the distinction between function an pattern bindings,
> but is not clear about the position of the type annotation. It merely
> states "the user must be careful to affix these [pattern bindings] with
> type signatures to retain full overloading".
>
> Olaf
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.



-- 
brandon s allbery kf8nh
allbery.b at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20211007/7e2076dc/attachment.html>