[Git][ghc/ghc][master] Preserve orientation when unifying kinds
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Wed Dec 25 06:44:28 UTC 2024
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
63d63f9d by Simon Peyton Jones at 2024-12-25T01:43:45-05:00
Preserve orientation when unifying kinds
This MR fixes yet another manifestation of the trickiness caused
by Note [Fundeps with instances, and equality orientation].
I wish there was a more robust way to do this, but this fix is
a definite improvement.
Fixes #25597
- - - - -
7 changed files:
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/rep-poly/RepPolyMcGuard.stderr
- testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
- testsuite/tests/rep-poly/T12709.stderr
- + testsuite/tests/typecheck/should_compile/T25597.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -2234,7 +2234,7 @@ to our new cbv. This is actually done by `break_given` in
`GHC.Tc.Solver.Monad.checkTypeEq`.
Note its orientation: The type family ends up on the left; see
-Note [Orienting TyFamLHS/TyFamLHS]d. No special treatment for
+Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for
CycleBreakerTvs is necessary. This scenario is now easily soluble, by using
the first Given to rewrite the Wanted, which can now be solved.
@@ -2906,8 +2906,7 @@ arising from injectivity improvement (#12522). Suppose we have
type instance F (a, Int) = (Int, G a)
where G is injective; and wanted constraints
- [W] TF (alpha, beta) ~ fuv
- [W] fuv ~ (Int, <some type>)
+ [W] F (alpha, beta) ~ (Int, <some type>)
The injectivity will give rise to constraints
@@ -2923,8 +2922,8 @@ so that the fresh unification variable will be eliminated in
favour of alpha. If we instead had
[W] alpha ~ gamma1
then we would unify alpha := gamma1; and kick out the wanted
-constraint. But when we grough it back in, it'd look like
- [W] TF (gamma1, beta) ~ fuv
+constraint. But when we substitute it back in, it'd look like
+ [W] F (gamma1, beta) ~ fuv
and exactly the same thing would happen again! Infinite loop.
This all seems fragile, and it might seem more robust to avoid
@@ -2981,8 +2980,9 @@ improveWantedTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
-- Work-item is a Wanted
improveWantedTopFunEqs fam_tc args ev rhs_ty
= do { eqns <- improve_wanted_top_fun_eqs fam_tc args rhs_ty
- ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs_ty
- , ppr eqns ])
+ ; traceTcS "improveTopFunEqs" (vcat [ text "lhs:" <+> ppr fam_tc <+> ppr args
+ , text "rhs:" <+> ppr rhs_ty
+ , text "eqns:" <+> ppr eqns ])
; unifyFunDeps ev Nominal $ \uenv ->
uPairsTcM (bump_depth uenv) (reverse eqns) }
-- Missing that `reverse` causes T13135 and T13135_simple to loop.
@@ -3005,6 +3005,8 @@ improve_wanted_top_fun_eqs fam_tc lhs_tys rhs_ty
= do { fam_envs <- getFamInstEnvs
; top_eqns <- improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
; let local_eqns = improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty
+ ; traceTcS "improve_wanted_top_fun_eqs" $
+ vcat [ ppr fam_tc, text "local_eqns" <+> ppr local_eqns, text "top_eqns" <+> ppr top_eqns ]
; return (local_eqns ++ top_eqns) }
| otherwise -- No injectivity
@@ -3035,14 +3037,14 @@ improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
-- The order of unsubstTvs is important; it must be
-- in telescope order e.g. (k:*) (a:k)
- ; subst <- instFlexiX subst unsubstTvs
+ ; subst1 <- instFlexiX subst unsubstTvs
-- If the current substitution bind [k -> *], and
-- one of the un-substituted tyvars is (a::k), we'd better
-- be sure to apply the current substitution to a's kind.
-- Hence instFlexiX. #13135 was an example.
- ; if apartnessCheck (substTys subst branch_lhs_tys) branch
- then return (mkInjectivityEqns inj_args (map (substTy subst) branch_lhs_tys) lhs_tys)
+ ; if apartnessCheck (substTys subst1 branch_lhs_tys) branch
+ then return (mkInjectivityEqns inj_args (map (substTy subst1) branch_lhs_tys) lhs_tys)
-- NB: The fresh unification variables (from unsubstTvs) are on the left
-- See Note [Improvement orientation]
else return [] }
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2483,7 +2483,14 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
do { def_eqs <- readTcRef def_eq_ref -- Capture current state of def_eqs
-- Attempt to unify kinds
- ; co_k <- uType (mkKindEnv env ty1 ty2) (typeKind ty2) (tyVarKind tv1)
+ -- When doing so, be careful to preserve orientation;
+ -- see Note [Kind Equality Orientation] in GHC.Tc.Solver.Equality
+ -- and wrinkle (W2) in Note [Fundeps with instances, and equality orientation]
+ -- in GHC.Tc.Solver.Dict
+ -- Failing to preserve orientation led to #25597.
+ ; let kind_env = unSwap swapped (mkKindEnv env) ty1 ty2
+ ; co_k <- unSwap swapped (uType kind_env) (tyVarKind tv1) (typeKind ty2)
+
; traceTc "uUnfilledVar2 ok" $
vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
, ppr ty2 <+> dcolon <+> ppr (typeKind ty2)
=====================================
testsuite/tests/rep-poly/RepPolyMcGuard.stderr
=====================================
@@ -1,12 +1,12 @@
-
RepPolyMcGuard.hs:30:16: error: [GHC-55287]
- • The first argument of the rebindable syntax operator ‘guard’
+ • The first argument of the rebindable syntax operator ‘(>>)’
arising from a statement in a monad comprehension
does not have a fixed runtime representation.
Its type is:
- a0 :: TYPE rep0
+ ma0 :: TYPE rep0
Cannot unify ‘rep’ with the type variable ‘rep0’
because the former is not a concrete ‘RuntimeRep’.
• In a stmt of a monad comprehension: undefined
In the expression: [() | undefined]
In an equation for ‘foo’: foo _ = [() | undefined]
+
=====================================
testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
=====================================
@@ -1,4 +1,3 @@
-
RepPolyRecordUpdate.hs:7:35: error: [GHC-55287]
• The newtype constructor pattern
does not have a fixed runtime representation.
@@ -14,7 +13,7 @@ RepPolyRecordUpdate.hs:7:35: error: [GHC-55287]
X a :: TYPE rep
RepPolyRecordUpdate.hs:13:9: error: [GHC-55287]
- • The record update at field ‘fld’
+ • The argument ‘fld’ of ‘MkX’
does not have a fixed runtime representation.
Its type is:
a :: TYPE rep0
@@ -25,3 +24,4 @@ RepPolyRecordUpdate.hs:13:9: error: [GHC-55287]
and data constructor ‘MkX’.
In the expression: x {fld = meth ()}
In an equation for ‘upd’: upd x = x {fld = meth ()}
+
=====================================
testsuite/tests/rep-poly/T12709.stderr
=====================================
@@ -1,6 +1,5 @@
-
T12709.hs:28:13: error: [GHC-55287]
- • The argument ‘1’ of ‘(+)’
+ • The argument ‘1 + 2 + 3’ of ‘(+)’
does not have a fixed runtime representation.
Its type is:
a0 :: TYPE rep0
@@ -13,3 +12,4 @@ T12709.hs:28:13: error: [GHC-55287]
u :: Num (a :: TYPE rep) => a
u = 1 + 2 + 3 + 4
in BUB u u
+
=====================================
testsuite/tests/typecheck/should_compile/T25597.hs
=====================================
@@ -0,0 +1,74 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T25597 where
+import Data.Kind (Type)
+
+data Env (f :: k -> Type) (as :: [k]) where
+ ENil :: Env f '[]
+ ECons :: f a -> Env f as -> Env f (a ': as)
+
+data Sig2 k = [k] :~> k
+
+data DimSimple (s :: Sig2 k) where
+ DimSimple :: OfLength as -> DimSimple (as ':~> a)
+
+data OfLength as where
+ LZ :: OfLength '[]
+ LS :: OfLength as -> OfLength (a ': as)
+
+class LiftOfLength f as t | t -> as where
+ liftOfLength :: OfLength as -> f t
+
+instance t ~ (as ':~> a) => LiftOfLength DimSimple as t where
+ liftOfLength = undefined
+
+data EnvI (sem :: [k] -> k -> Type) (a :: k)
+
+type family Func sem as r where
+ Func sem '[] r = r
+ Func sem (a ': as) r = sem a -> Func sem as r
+
+
+type family FuncU (sem :: [k] -> k -> Type) (ss :: [Sig2 k])
+ (r :: k) = res | res -> sem r where
+ FuncU sem '[] r = EnvI sem r
+ FuncU sem ((as ':~> a) ': ss) r = Func (EnvI sem) as (EnvI sem a)
+ -> FuncU sem ss r
+
+lifts :: Env DimSimple ss -> FuncU sem ss r
+lifts _ = undefined
+
+-- The following version specialized to singletons does not cause an issue
+type family FuncS (sem :: [k] -> k -> Type) (s :: Sig2 k)
+ (r :: k) = res | res -> sem r where
+ FuncS sem (as ':~> a) r = Func (EnvI sem) as (EnvI sem a) -> EnvI sem r
+
+
+lift :: DimSimple s -> FuncS sem s r
+lift _ = undefined
+
+-- The following code causes non termination of type checking in GHC 9.2, 9.8, 9.10, and 9.12
+f :: (EnvI Sem a -> EnvI Sem b) -> EnvI Sem (a -> b)
+f = lifts (ECons (liftOfLength (LS LZ)) ENil)
+
+data Sem (env :: [Type]) a
+
+-- Following versions have no issues in GHC 9.8
+-- (I haven't tested other compilers but expect the similar results)
+-- f = undefined $ lifts (ECons (liftOfLength (LS LZ)) ENil)
+-- f = let h = lifts (ECons (liftOfLength (LS LZ)) ENil) in h
+-- f = h where h = lifts (ECons (liftOfLength (LS LZ)) ENil)
+-- f = lifts (ECons (DimSimple (LS LZ)) ENil)
+-- f = lifts d where {d :: Env DimSimple '[ '[a] :~> b ]; d = (ECons (liftOfLength (LS LZ)) ENil) }
+-- f = lift (liftOfLength (LS LZ))
+-- f = (lifts :: Env DimSimple ss -> FuncU Sem ss r) (ECons (liftOfLength (LS LZ)) ENil)
+-- f without its signature
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -931,3 +931,4 @@ test('T23501b', normal, compile, [''])
test('T25266', normal, compile, [''])
test('T25266a', normal, compile_fail, [''])
test('T25266b', normal, compile, [''])
+test('T25597', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/63d63f9d3e074c3bcf5b526ee14e50cb2b6b9d70
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/63d63f9d3e074c3bcf5b526ee14e50cb2b6b9d70
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20241225/10cec57a/attachment-0001.html>
More information about the ghc-commits
mailing list