GHC 9.6

[Ericson2314]

No description provided.

[erikd]

Thanks @Ericson2314 !

[ncfavier]

Builds and tests fine with GHC 9.2. GHC 9.4 complains with

test/test.hs:159:1: error:
    More than one instance found for GEq (a_0), and unsure what to do. Please report this.
    |
159 | deriveGEq ''Spleeb
    | ^^^^^^^^^^^^^^^^^^

[ncfavier]

The failing data type is

data Spleeb a b where
    P :: a Double -> Qux b -> Spleeb a b

The difference between versions seems to be that reifyInstancesWithRigids [a, b] ''GEq a returns [] in GHC 9.2 (which is expected because a is a rigid type variable), but with GHC 9.4 it returns

InstanceD Nothing [AppT (ConT Data.GADT.Internal.GEq) (VarT a_6989586621679027108),AppT (ConT Data.GADT.Internal.GEq) (VarT b_6989586621679027109)] (AppT (ConT Data.GADT.Internal.GEq) (SigT (AppT (AppT (ConT GHC.Generics.:*:) (VarT a_6989586621679027108)) (VarT b_6989586621679027109)) (AppT (AppT ArrowT (VarT k_6989586621679027107)) StarT))) []
InstanceD Nothing [AppT (ConT Data.GADT.Internal.GEq) (VarT f_6989586621679030688),AppT (ConT Data.GADT.Internal.GEq) (VarT g_6989586621679030689)] (AppT (ConT Data.GADT.Internal.GEq) (SigT (AppT (AppT (ConT GHC.Generics.:+:) (VarT f_6989586621679030688)) (VarT g_6989586621679030689)) (AppT (AppT ArrowT (VarT k_6989586621679030687)) StarT))) []
InstanceD Nothing [] (AppT (ConT Data.GADT.Internal.GEq) (SigT (AppT (ConT Data.Type.Equality.:~:) (VarT a_6989586621679030691)) (AppT (AppT ArrowT (VarT k_6989586621679030690)) StarT))) []
InstanceD Nothing [] (AppT (ConT Data.GADT.Internal.GEq) (SigT (AppT (ConT Data.Type.Equality.:~~:) (VarT a_6989586621679030694)) (AppT (AppT ArrowT (VarT k_6989586621679030693)) StarT))) []
InstanceD Nothing [AppT (ConT Data.GADT.Internal.GEq) (VarT a_6989586621679030696),AppT (ConT Data.GADT.Internal.GEq) (VarT b_6989586621679030697)] (AppT (ConT Data.GADT.Internal.GEq) (SigT (AppT (AppT (ConT Data.Functor.Product.Product) (VarT a_6989586621679030696)) (VarT b_6989586621679030697)) (AppT (AppT ArrowT (VarT k_6989586621679030695)) StarT))) []
InstanceD Nothing [AppT (ConT Data.GADT.Internal.GEq) (VarT a_6989586621679030876),AppT (ConT Data.GADT.Internal.GEq) (VarT b_6989586621679030877)] (AppT (ConT Data.GADT.Internal.GEq) (SigT (AppT (AppT (ConT Data.Functor.Sum.Sum) (VarT a_6989586621679030876)) (VarT b_6989586621679030877)) (AppT (AppT ArrowT (VarT k_6989586621679030875)) StarT))) []

So my guess is that GHC 9.4 got smarter, and the Skolem trick in

dependent-sum-template/src/Data/GADT/TH/Internal.hs

Lines 37 to 38 in 9a83b0a

	-- Do not export this type family, it must remain empty. It's used as a way to trick GHC into not unifying certain type variables.
	type family Skolem :: k -> k

does not trick it any more. @cgibbard any ideas?

EDIT: looking at the returned instances, it seems like it only returns the instances that unify with GEq (s a), hence somehow treating Skolem as a metavariable. GHC bug?

[ncfavier]

Opened a GHC bug with a minimal reproducer https://gitlab.haskell.org/ghc/ghc/-/issues/23743

[ali-abrar]

Given the ghc issue, it might be better to support 9.6 and skip 9.2 and 9.4

[ali-abrar]

@Ericson2314 if you're ok with the direction of #6, please close this.