GHC 9.2.2?

[jhenahan]

I'm on a sabbatical, and I'm devoting some of that time to slamming myself face first into the bleeding edge of stuff that I think is neat in Haskell. I'm presently throwing myself at getting in-other-words building on 9.2.2 and then going on to write some libraries on top of it, so I mostly just want to use this ticket to track my findings and potentially get your input on how to fix things that are broken.

It'll take me a bit to get spun up on all the machinery here, so any pointers are highly valued. :)

Nits:

• StarIsType warnings (easy fix)

Broken stuff:

Carrier instances

• Control.Effect.Internal.Newtype.UnwrapTopC (looks like UnwrappedEff is hanging around too long, maybe?)
• Control.Effect.Writer.ListenIntoEndoListenC: Could not deduce (Member (Tell (Endo o)) (Derivs m)) ... from the context: (Monoid o, HeadEffs '[Listen (Endo o), Tell (Endo o)] m)
• Control.Effect.Writer.WriterIntoEndoWriterC: As above
• Control.Effect.Union.UnionizeHeadC

  Could not deduce (Member (Union b) (Derivs m))
    arising from a use of ‘inj’
  from the context: (HeadEff (Union b) m, KnownList b)
  
  Could not deduce: Derivs m
                    ~ (_e0 : StripPrefix '[Union b] (Derivs m))
  from the context: (HeadEff (Union b) m, KnownList b)
  Expected: Union (Derivs m) z a
    Actual: Union (_e0 : StripPrefix '[Union b] (Derivs m)) z a
  

interpretViaHandler uses

I suspect these are all tied up in the Carrier instances, but I don't understand the machinery well enough yet to fix it.

• Control.Effect.Trace.traceIntoTell: Could not deduce (Member (Tell String) (Derivs m)) ... from the context: HeadEff (Tell String) m
• Control.Effect.Writer.tellIntoEndoTell: Could not deduce (Member (Tell (Endo o)) (Derivs m)) ... from the context: (Monoid o, HeadEff (Tell (Endo o)) m)
• Control.Effect.Writer.listenIntoEndoListen: As above, plus Listen (Endo o)
• Control.Effect.Writer.writerIntoEndoWriter: As above, plus Pass (Endo o)

Others

• Control.Effect.Writer.tellIntoTell and Control.Effect.Writer.tellIntoTellSimple: Could not deduce (Member (Tell o') (Derivs m)), which I expect is just more of the carrier issue poking through.

[KingoftheHomeless]

Some of these look so weird I'm inclined to call it GHC bugs. For example Could not deduce (Member (Tell String) (Derivs m)) ... from the context: HeadEff (Tell String) m is absolutely something GHC should be able to prove. I'll look into it, but not today; I'll hopefully be able to tomorrow.

[jhenahan]

Yeah, that seems really unusual, right? Usually GHC has the ones you can do in your head well in hand. 😆 I have a suspicion that perhaps the root of it is all in UnionizeHeadC.

[KingoftheHomeless]

Using the following:

data Dict (c :: Constraint) where
  Dict :: c => Dict c

Error:

wow :: ( new ~ '[e]
       , Append new (StripPrefix new (Derivs m)) ~ Derivs m)
    => Proxy m
    -> Dict (Member e (Derivs m))
wow _ = Dict

No error:

wow :: ( new ~ '[e]
       , r ~ Derivs m
       , Append new (StripPrefix new (Derivs m)) ~ Derivs m)
    => Proxy m
    -> Dict (Member e (Derivs m))
wow _ = Dict

Note how I did nothing but introduce an unused variable with a type equality constraint to Derivs m!

This is a GHC bug.
I've never reported one before. Have to brush up on what the proper process is.

[KingoftheHomeless]

In the meantime, I'm trying to figure out a workaround without resorting to the Threaders solution of introducing a parameter to IntroConsistent and friends solely to get a polymorphic type variable for the r ~ Derivs m constraint. No luck yet; tried leveraging quantified constraints, and turning simple constraint synonyms into classes, and a mix of the two, without any success.
Here's a minimal reproducer to play around with (given all necessary extensions switched on):

{-# LANGUAGE ConstraintKinds, DataKinds, TypeOperators, GADTs #-}
{-# LANGUAGE TypeFamilies, KindSignatures, FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Reproducer where

import Data.Kind (Type, Constraint)

data Dict (c :: Constraint) where
  Dict :: c => Dict c

class Foo (e :: Type) (r :: [Type])

instance Foo e (e ': r)

type family R :: [Type]
type family F (a :: [Type]) :: [Type]

compiles :: (R ~ Int ': F R, r ~ R)
         => Dict (Foo Int R)
compiles = Dict

errors :: (R ~ Int ': F R)
       => Dict (Foo Int R)
errors = Dict

[KingoftheHomeless]

Haven't been able to find a GHC issue that quite fits this bill, so created a new one: https://gitlab.haskell.org/ghc/ghc/-/issues/21473

[KingoftheHomeless]

Alright, with GHC 9.2.3 released and in stackage nightly, I'm going to revisit this issue and try to get it closed.

[KingoftheHomeless]

Turns out the StarIsType issues were all that remained. With that fixed, in-other-words compiles without warnings with GHC 9.2.3. 0.2.1.1 will be released on Hackage soon.