Simon Peyton Jones pushed to branch wip/T26256 at Glasgow Haskell Compiler / GHC Commits: d9959658 by Simon Peyton Jones at 2025-08-04T17:49:12+01:00 Take more care in zonkEqTypes on AppTy/AppTy This patch fixes #26256. See Note [zonkEqTypes and the PKTI] in GHC.Tc.Solver.Equality - - - - - 6 changed files: - compiler/GHC/Tc/Solver/Equality.hs - + testsuite/tests/partial-sigs/should_compile/T26256.hs - + testsuite/tests/partial-sigs/should_compile/T26256.stderr - testsuite/tests/partial-sigs/should_compile/all.T - + testsuite/tests/typecheck/should_compile/T26256a.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -197,12 +197,8 @@ zonkEqTypes ev eq_rel ty1 ty2 then tycon tc1 tys1 tys2 else bale_out ty1 ty2 - go ty1 ty2 - | Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1 - , Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2 - = do { res_a <- go ty1a ty2a - ; res_b <- go ty1b ty2b - ; return $ combine_rev mkAppTy res_b res_a } + -- If you are temppted to add a case for AppTy/AppTy, be careful + -- See Note [zonkEqTypes and the PKTI] go ty1@(LitTy lit1) (LitTy lit2) | lit1 == lit2 @@ -278,6 +274,32 @@ zonkEqTypes ev eq_rel ty1 ty2 combine_rev f (Right tys) (Right ty) = Right (f ty tys) +{- Note [zonkEqTypes and the PKTI] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Because `zonkEqTypes` does /partial/ zonking, we need to be very careful +to maintain the Purely Kinded Type Invariant: see GHC.Tc.Gen/HsType +HsNote [The Purely Kinded Type Invariant (PKTI)]. + +In #26256 we try to solve this equality constraint: + Int :-> Maybe Char ~# k0 Int (m0 Char) +where m0 and k0 are unification variables, and + m0 :: Type -> Type +It happens that m0 was already unified + m0 := (w0 :: kappa) +where kappa is another unification variable that is also already unified: + kappa := Type->Type. +So the original type satisifed the PKTI, but a partially-zonked form + k0 Int (w0 Char) +does not!! (This a bit reminiscent of Note [mkAppTyM].) + +The solution I have adopted is simply to make `zonkEqTypes` bale out on `AppTy`. +After all, it's only supposed to be a quick hack to see if two types are already +equal; if we bale out we'll just get into the "proper" canonicaliser. + +The only tricky thing about this approach is that it relies on /omitting/ +code -- for the AppTy/AppTy case! Hence this Note +-} + {- ********************************************************************* * * * canonicaliseEquality ===================================== testsuite/tests/partial-sigs/should_compile/T26256.hs ===================================== @@ -0,0 +1,23 @@ +{-# LANGUAGE GHC2021 #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE PartialTypeSignatures #-} + +module M (go) where + +import Data.Kind + +type Apply :: (Type -> Type) -> Type +data Apply m + +type (:->) :: Type -> Type -> Type +type family (:->) where (:->) = (->) + +f :: forall (k :: Type -> Type -> Type) (m :: Type -> Type). + k Int (m Char) -> k Bool (Apply m) +f = f + +x :: Int :-> Maybe Char +x = x + +go :: Bool -> _ _ +go = f x ===================================== testsuite/tests/partial-sigs/should_compile/T26256.stderr ===================================== @@ -0,0 +1,8 @@ +T26256.hs:22:15: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)] + • Found type wildcard ‘_’ standing for ‘Apply :: (* -> *) -> *’ + • In the type signature: go :: Bool -> _ _ + +T26256.hs:22:17: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)] + • Found type wildcard ‘_’ standing for ‘Maybe :: * -> *’ + • In the first argument of ‘_’, namely ‘_’ + In the type signature: go :: Bool -> _ _ ===================================== testsuite/tests/partial-sigs/should_compile/all.T ===================================== @@ -108,3 +108,4 @@ test('T21667', normal, compile, ['']) test('T22065', normal, compile, ['']) test('T16152', normal, compile, ['']) test('T20076', expect_broken(20076), compile, ['']) +test('T26256', normal, compile, ['']) ===================================== testsuite/tests/typecheck/should_compile/T26256a.hs ===================================== @@ -0,0 +1,19 @@ +{-# LANGUAGE GHC2021 #-} +{-# LANGUAGE TypeFamilies #-} + +module T26256 (go) where + +import Data.Kind + +class Cat k where (<<<) :: k a b -> k x a -> k x b +instance Cat (->) where (<<<) = (.) +class Pro k p where pro :: k a b s t -> p a b -> p s t +data Hiding o a b s t = forall e. Hiding (s -> o e a) +newtype Apply e a = Apply (e a) + +type (:->) :: Type -> Type -> Type +type family (:->) where + (:->) = (->) + +go :: (Pro (Hiding Apply) p) => (s :-> e a) -> p a b -> p s t +go sea = pro (Hiding (Apply <<< sea)) ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -940,3 +940,4 @@ test('T26020', normal, compile, ['']) test('T26020a', [extra_files(['T26020a_help.hs'])], multimod_compile, ['T26020a', '-v0']) test('T25992', normal, compile, ['']) test('T14010', normal, compile, ['']) +test('T26256a', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d9959658d426a5352c0dfccdc54d1f2d... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d9959658d426a5352c0dfccdc54d1f2d... You're receiving this email because of your account on gitlab.haskell.org.