[Haskell-cafe] type error when specializing lens zooms in ghc >= 9.0

[Olaf Klinke]

On Thu, 2023-06-01 at 17:55 +0300, Bryan Richter wrote:
> And in case it proves intractable to provide concise, useful error
> messages, perhaps having entries at https://errors.haskell.org (with
> examples!) would also be helpful.
> 

The thing is, the error message is rather general, which was my
original complaint. I haven't got a GHC-9.6.1 installation, so what is
the error code when compiling the following minimal example? More
importantly, how many situations completely unrelated to simplified
subsumption produce the same error code? If there are many such
situations, then making the errors.haskell.org entry of the error code
point to simplified subsumption would mislead too many programmers,
wouldn't it? 

{-# LANGUAGE RankNTypes #-}

type Void = forall t. t

{-- does compile with ghc < 9 but not with ghc >= 9,
    error message is of the form

    Couldn't match type <concrete type> with 
    <Rank-2 type that unifies with <concrete type> 
    by specializing universally quantified type variables>
--}
final :: Void -> ()
final = (id :: () -> ())

-- eta-expanded version of final, 
-- does compile with ghc >= 9
finalEta :: Void -> ()
finalEta x = id x

Having produced this example, I do acknowledge that simplified
subsumption is an improvement. The fact that ghc 8 did accept the
equation final=id is indeed weird. 

Olaf


> On Mon, 15 May 2023 at 18:07, Olaf Klinke <olf at aatal-apotheke.de> wrote:
> 
> > On Fri, 2023-05-12 at 17:13 -0400, Brandon Allbery wrote:
> > > My first suspicion would be simplified subsumption. Try eta-expanding
> > them.
> > > 
> > 
> > Indeed, the eta-expanded versions do compile with GHC >= 9.
> > Now I remember that I've fallen into a similar trap before [1] (and
> > Brandon offered the right hint back then, too. Thanks, Brandon!)
> > So let me re-cap:
> > (1) Haskell is not a category: there are types a, b, c
> >     and morphisms f :: a -> b, g :: b -> c
> >     such that g.f is not a morphism.
> > (2) Haskell is not a lambda calculus [2]: There are terms f such that
> >     \x -> f x
> >     belongs to the calculus but f does not.
> > 
> > Personally, I would already call the situation improved when the
> > compiler instead of Brandon could tell me the fix. From the discussion
> > [3]:
> > 
> > > The most interesting thing I've learned from the lengthy threads,
> > > along with deficiencies in the testing process for ecosystem
> > > breakage, is how much absolute confusion there is over how rank-n-
> > > types work, and the limitations and complexities of algorithms
> > > pertaining to them. Now that they are in widespread use and on by
> > > default in ghc, it seems like an important case where user education
> > > is warranted.
> > 
> > I'd love to be educated. And I'd be very pleased if helpful compiler
> > error messages were the first entry point for that, so that I can spare
> > the patient and helpful Haskell Cafe members some time.
> > 
> > Olaf
> > 
> > [1]
> > https://mail.haskell.org/pipermail/haskell-cafe/2023-February/135903.html
> > [2]
> > https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst#costs-and-drawbacks
> > [3] https://github.com/ghc-proposals/ghc-proposals/pull/287
> > 
> > that apparently I have not managed to form an in
> > 
> > > On Fri, May 12, 2023 at 5:10 PM Olaf Klinke <olf at aatal-apotheke.de>
> > wrote:
> > > > 
> > > > Dear Cafe,
> > > > 
> > > > I'm an infrequent lens user so please forgive me if the below problem
> > > > has a trivial solution.
> > > > 
> > > > For a long time the documentation of Control.Lens.Zoom has been
> > > > claiming that 'zoom' and 'magnify' can be specialized to the following
> > > > types.
> > > > 
> > > > {-# LANGUAGE RankNTypes #-}
> > > > -- Type error with GHC 9.0.2 or 9.2.7, okay with GHC 8.8.4
> > > > import Control.Lens.Zoom (zoom,magnify)
> > > > import Control.Lens.Type (Lens')
> > > > import Control.Monad.RWS (RWS)
> > > > zoomRWS ::    Monoid w => Lens' s s' -> RWS r w s' a -> RWS r w s a
> > > > zoomRWS = zoom
> > > > magnifyRWS :: Monoid w => Lens' r r' -> RWS r' w s a -> RWS r w s a
> > > > magnifyRWS = magnify
> > > > 
> > > > Indeed GHC 8.8.4 compiles this happily (on lens-4.18.1), but 9.0.2 (on
> > > > lens-5.0.1) throws nearly undecipherable errors, claiming that Lens'
> > > > can not be matched with some more specialized type involving Magnified
> > > > and LensLike.
> > > > The source of Control.Lens.Zoom does not differ substantially between
> > > > 4.18.1 and 5.0.1 so my guess is it is a type checker issue. Can anyone
> > > > explain? On which bug tracker should I raise this issue, if it is
> > > > indeed a valid one?
> > > > (I pulled the above versions from stackage lts-16.31, -19.5 and -20.20,
> > > > respectively and compiled with stack.)
> > > > 
> > > > Thanks
> > > > 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.
> > > 
> > > 
> > > 
> > 
> > 
> > _______________________________________________
> > 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.