Simon Peyton Jones pushed to branch wip/T26543b at Glasgow Haskell Compiler / GHC Commits: 96bc4a6e by Simon Peyton Jones at 2026-09-27T18:39:25+01:00 Wibbles - - - - - 9 changed files: - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Utils/Unify.hs - testsuite/tests/default/default-fail05.stderr - testsuite/tests/ghci.debugger/scripts/T14628.stderr - testsuite/tests/indexed-types/should_fail/T1897b.stderr - testsuite/tests/typecheck/should_fail/T22707.stderr - + testsuite/tests/typecheck/should_fail/T26543a.hs - testsuite/tests/typecheck/should_fail/all.T Changes: ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -55,7 +55,6 @@ module GHC.Core.TyCo.FVs ) where import GHC.Prelude -import GHC.Exts( inline ) import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView ) @@ -852,8 +851,11 @@ invisibleVarsOfTypes = foldr (unionVarSet . invisibleVarsOfType) emptyVarSet {- Note [Any-free-var folder] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The "any-free-var" folders take a `check_fv` predicate (TyCoVar -> Bool) and -check if any free variable of the type/coercion satisfies it. Our main folders -look like: +check if any /deep/ free variable of the type/coercion satisfies it. So + + anyFreeVarsOfType p ty = anyVarSet p (tyCoVarsOfType ty) + +Our main folders look like: afv_type :: Type -> FV (BoundVars, TyVar -> Bool) Any @@ -871,7 +873,7 @@ nice tight loops. {-# INLINE afvFolder #-} -- See Note [Any-free-var folder] afvFolder :: TyCoFolder (FV (BoundVars, TyCoVar -> Bool) DM.Any) -- 'afvFolder' is short for "any-free-var folder", good for checking --- if any shallow free var of a type satisfies a predicate `check_fv` +-- if any /deep/ free var of a type satisfies a predicate `check_fv` -- The "env" of the (FV env Any) is a pair (bvs,pred) of -- the bound variables (which are definitely not free), and -- an "interesting var" predicate which the client supplies @@ -881,8 +883,11 @@ afvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and synonyms] , tcf_hole = do_hole , tcf_tycobinder = addBndrSelectiveFV } where - do_tcv tv = MkFV $ \ (bvs,check_fv) -> - Any (not (tv `elemVarSet` bvs) && check_fv tv) + -- Check the variable itself with check_fv, + -- and check its kind (this is a deep folder) + do_tcv tcv = MkFV $ \ (bvs,check_fv) -> + Any (not (tcv `elemVarSet` bvs) && + (check_fv tcv || runAny check_fv (afv_type (varType tcv)))) do_hole hole = do_tcv (coHoleCoVar hole) afv_type :: Type -> FV (BoundVars, TyVar -> Bool) DM.Any @@ -892,7 +897,7 @@ afv_co :: Coercion -> FV (BoundVars, TyVar -> Bool) DM.Any runAny :: (TyVar -> Bool) -> FV (BoundVars, TyCoVar -> Bool) DM.Any -> Bool {-# INLINE runAny #-} -runAny check_fv fvs = DM.getAny $ runFV fvs (emptyVarSet, check_fv) +runAny check_fv fvs = DM.getAny (runFV fvs (emptyVarSet, check_fv)) anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool {-# INLINE anyFreeVarsOfType #-} ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -2196,10 +2196,9 @@ qlUnify ty1 ty2 -- the main point of QuickLook (allowing meta-variables to be unified -- with qualified types). - go' (TyVarTy tv) ty2 - | isQLInstTyVar tv = go_kappa tv ty2 - go' ty1 (TyVarTy tv) - | isQLInstTyVar tv = go_kappa tv ty1 + -- Type variables; see (UQL6) in Note [QuickLook unification] + go' (TyVarTy tv) ty2 | isQLInstTyVar tv = go_kappa tv ty2 + go' ty1 (TyVarTy tv) | isQLInstTyVar tv = go_kappa tv ty1 go' (CastTy ty1 _) ty2 = go ty1 ty2 go' ty1 (CastTy ty2 _) = go ty1 ty2 @@ -2242,6 +2241,8 @@ qlUnify ty1 ty2 ---------------- go_flexi kappa ty2 -- ty2 is zonked + | isConcreteTyVar kappa -- See (UQL7) in Note [QuickLook unification] + = return () | anyFreeVarsOfType (== kappa) ty2 = return () -- Occurs check | otherwise @@ -2340,6 +2341,22 @@ That is the entire point of qlUnify! Wrinkles: constraint arrows =>, so that (UQL4) applies to them as well. See Note [Multiplicity in deep subsumption]. +(UQL6) What if `qlUnify` sees a regular (monotyped) unification variable, `alpha`, rather + than an instantiation variable `kappa`? Thus (alpha ~ ty). It's tempting to just + unify it, but the regular, on-the-fly unifier has lots of careful checks (levels, + concreteness etc). In regular unification it doesn't matter whether we unify on-the-fly + or later -- it's just an efficiency issue -- but here it matters because `qlUnify` has + /user-visible/ consequences. This led to #26543. + + The simplest thing is to say that `qlUnify` unifies /only/ instantiation variables + (see calls to `isQLInstTyVar`). We could be more ambitious, perhaps, in future. + +(UQL7) If `qlUnify` sees a concrete `kaapa`, thus + kappa[conc] ~ some-type + we just give up. It's tiresome to do all the checks for concreteness; and concrete + type variables are never unified with polytypes, so it's fine to leave it for the + regular unifier. + Sadly discarded design alternative ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It is very tempting to use `unifyType` rather than `qlUnify`, killing off the ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -3596,7 +3596,6 @@ matchExpectedFunKind hs_ty n k = go n k data UnifyCheckCaller = UC_OnTheFly -- Called from the on-the-fly unifier - | UC_QuickLook -- Called from Quick Look | UC_Solver -- Called from constraint solver -- | The result type of 'simpleUnifyCheck'. @@ -3649,9 +3648,7 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs lhs_tv_is_concrete = isConcreteTyVar lhs_tv lhs_tv_nm = tyVarName lhs_tv - forall_ok = case caller of - UC_QuickLook -> isQLInstTyVar lhs_tv - _ -> isRuntimeUnkTyVar lhs_tv + forall_ok = isRuntimeUnkTyVar lhs_tv -- This fam_ok thing relates to a very specific perf problem -- See Note [Prevent unification with type families] @@ -3660,7 +3657,6 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs -- see if it bites us) fam_ok = case caller of UC_Solver -> True - UC_QuickLook -> True UC_OnTheFly -> False rhs_tcv_is_bad tcv ===================================== testsuite/tests/default/default-fail05.stderr ===================================== @@ -1,45 +1,45 @@ default-fail05.hs:11:10: error: [GHC-39999] - • Ambiguous type variable ‘f0’ arising from a use of ‘toList’ - prevents the constraint ‘(Foldable f0)’ from being solved. - Probable fix: use a type annotation to specify what ‘f0’ should be. + • Ambiguous type variable ‘t0’ arising from a use of ‘toList’ + prevents the constraint ‘(Foldable t0)’ from being solved. + Probable fix: use a type annotation to specify what ‘t0’ should be. Potentially matching instances: instance Foldable (Either a) -- Defined in ‘GHC.Internal.Data.Foldable’ instance Foldable Maybe -- Defined in ‘GHC.Internal.Data.Foldable’ ...plus three others - ...plus 26 instances involving out-of-scope types + ...plus 11 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the first argument of ‘($)’, namely ‘toList’ In the first argument of ‘print’, namely ‘(toList $ pure 21)’ In a stmt of a 'do' block: print (toList $ pure 21) default-fail05.hs:11:19: error: [GHC-39999] - • Ambiguous type variable ‘f0’ arising from a use of ‘pure’ - prevents the constraint ‘(Applicative f0)’ from being solved. - Probable fix: use a type annotation to specify what ‘f0’ should be. + • Ambiguous type variable ‘t0’ arising from a use of ‘pure’ + prevents the constraint ‘(Applicative t0)’ from being solved. + Probable fix: use a type annotation to specify what ‘t0’ should be. Potentially matching instances: instance Applicative IO -- Defined in ‘GHC.Internal.Base’ instance Applicative Maybe -- Defined in ‘GHC.Internal.Base’ ...plus six others - ...plus 9 instances involving out-of-scope types + ...plus five instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the second argument of ‘($)’, namely ‘pure 21’ In the first argument of ‘print’, namely ‘(toList $ pure 21)’ In a stmt of a 'do' block: print (toList $ pure 21) default-fail05.hs:12:3: error: [GHC-39999] - • Ambiguous type variable ‘t0’ arising from a use of ‘traverse’ - prevents the constraint ‘(Traversable t0)’ from being solved. + • Ambiguous type variable ‘t1’ arising from a use of ‘traverse’ + prevents the constraint ‘(Traversable t1)’ from being solved. Relevant bindings include - main :: IO (t0 ()) (bound at default-fail05.hs:10:1) - Probable fix: use a type annotation to specify what ‘t0’ should be. + main :: IO (t1 ()) (bound at default-fail05.hs:10:1) + Probable fix: use a type annotation to specify what ‘t1’ should be. Potentially matching instances: instance Traversable (Either a) -- Defined in ‘GHC.Internal.Data.Traversable’ instance Traversable Maybe -- Defined in ‘GHC.Internal.Data.Traversable’ ...plus three others - ...plus 28 instances involving out-of-scope types + ...plus 13 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In a stmt of a 'do' block: traverse print (pure 42) In the expression: @@ -51,16 +51,16 @@ default-fail05.hs:12:3: error: [GHC-39999] traverse print (pure 42) default-fail05.hs:12:19: error: [GHC-39999] - • Ambiguous type variable ‘t0’ arising from a use of ‘pure’ - prevents the constraint ‘(Applicative t0)’ from being solved. + • Ambiguous type variable ‘t1’ arising from a use of ‘pure’ + prevents the constraint ‘(Applicative t1)’ from being solved. Relevant bindings include - main :: IO (t0 ()) (bound at default-fail05.hs:10:1) - Probable fix: use a type annotation to specify what ‘t0’ should be. + main :: IO (t1 ()) (bound at default-fail05.hs:10:1) + Probable fix: use a type annotation to specify what ‘t1’ should be. Potentially matching instances: instance Applicative IO -- Defined in ‘GHC.Internal.Base’ instance Applicative Maybe -- Defined in ‘GHC.Internal.Base’ ...plus six others - ...plus 9 instances involving out-of-scope types + ...plus five instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the second argument of ‘traverse’, namely ‘(pure 42)’ In a stmt of a 'do' block: traverse print (pure 42) ===================================== testsuite/tests/ghci.debugger/scripts/T14628.stderr ===================================== @@ -1,9 +1,9 @@ - -<interactive>:4:17: error: [GHC-25897] +<interactive>:4:7: error: [GHC-25897] • Couldn't match type ‘m’ with ‘(,) a0’ - Expected: StateT Int ((,) a0) () - Actual: StateT Int m () + Expected: (a0, ((), Int)) + Actual: m ((), Int) ‘m’ is an interactive-debugger skolem - • In the first argument of ‘runStateT’, namely ‘_result’ - In the second argument of ‘($)’, namely ‘runStateT _result 0’ + • In the second argument of ‘($)’, namely ‘runStateT _result 0’ In the expression: snd $ runStateT _result 0 + In an equation for ‘it’: it = snd $ runStateT _result 0 + ===================================== testsuite/tests/indexed-types/should_fail/T1897b.stderr ===================================== @@ -1,14 +1,14 @@ T1897b.hs:16:1: error: [GHC-83865] - • Couldn't match type: Depend b0 - with: Depend b - Expected: t (Depend b) -> Bool - Actual: t (Depend b0) -> Bool + • Couldn't match type: Depend a0 + with: Depend a + Expected: t (Depend a) -> Bool + Actual: t (Depend a0) -> Bool Note: ‘Depend’ is a non-injective type family. - The type variable ‘b0’ is ambiguous + The type variable ‘a0’ is ambiguous • In the ambiguity check for the inferred type for ‘isValid’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the inferred type - isValid :: forall {t :: * -> *} {b}. - (Foldable t, Bug b) => - t (Depend b) -> Bool + isValid :: forall {t :: * -> *} {a}. + (Foldable t, Bug a) => + t (Depend a) -> Bool ===================================== testsuite/tests/typecheck/should_fail/T22707.stderr ===================================== @@ -1,38 +1,11 @@ -T22707.hs:6:59: error: [GHC-25897] - • Couldn't match expected type ‘i1’ - with actual type ‘m0 - GHC.Internal.Types.LiftedRep GHC.Internal.Types.LiftedRep b0’ - ‘i1’ is a rigid type variable bound by - the type signature for: - t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) - at T22707.hs:5:1-47 - • In the expression: evalCont (t1 c) >>== \ ati1 -> return ati1 xa - In the second argument of ‘($)’, namely - ‘\ xa -> evalCont (t1 c) >>== \ ati1 -> return ati1 xa’ - In the second argument of ‘runCont’, namely - ‘(ati1tti2 $ \ xa -> evalCont (t1 c) >>== \ ati1 -> return ...)’ - • Relevant bindings include - ati1tti2 :: (a -> i1) -> i2 (bound at T22707.hs:6:16) - c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4) - t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) - (bound at T22707.hs:6:1) - T22707.hs:6:72: error: [GHC-25897] - • Couldn't match type ‘o’ - with ‘m0 - GHC.Internal.Types.LiftedRep - GHC.Internal.Types.LiftedRep - (m0 GHC.Internal.Types.LiftedRep GHC.Internal.Types.LiftedRep b0)’ + • Couldn't match type ‘i2’ with ‘a -> i1’ Expected: Cont - ((a -> i1) - -> m0 - GHC.Internal.Types.LiftedRep - GHC.Internal.Types.LiftedRep - (m0 GHC.Internal.Types.LiftedRep GHC.Internal.Types.LiftedRep b0)) + ((a -> i1) -> m0 (a -> i1) (a -> i1) (m0 (a -> i1) (a -> i1) b0)) i1 a Actual: Cont (i2 -> o) i1 a - ‘o’ is a rigid type variable bound by + ‘i2’ is a rigid type variable bound by the type signature for: t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) at T22707.hs:5:1-47 @@ -40,6 +13,9 @@ T22707.hs:6:72: error: [GHC-25897] In the first argument of ‘evalCont’, namely ‘(t1 c)’ In the first argument of ‘(>>==)’, namely ‘evalCont (t1 c)’ • Relevant bindings include + xa :: a (bound at T22707.hs:6:53) + ati1tti2 :: (a -> m0 (a -> i1) (a -> i1) b0) -> a -> i1 + (bound at T22707.hs:6:16) c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4) t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) (bound at T22707.hs:6:1) ===================================== testsuite/tests/typecheck/should_fail/T26543a.hs ===================================== @@ -0,0 +1,18 @@ +{-# LANGUAGE ImpredicativeTypes, PolyKinds #-} + +-- Should be rejected via an occurs-check in the kinds, +-- but was erroneously accpeted with ImpredicativeTypes +-- See !16566 + +module T26543 where + +import Data.Kind +import Data.Proxy + +h :: forall k (m :: k -> Type) (a :: k). (Proxy k, Proxy (m a)) +h = (Proxy, Proxy) + +use2 :: forall t. (Proxy t, Proxy t) -> () +use2 _ = () + +test = use2 h ===================================== testsuite/tests/typecheck/should_fail/all.T ===================================== @@ -763,3 +763,4 @@ test('T26861', normal, compile_fail, ['']) test('T26862', normal, compile_fail, ['']) test('T27210', normal, compile_fail, ['']) test('T26532', normal, compile_fail, ['']) +test('T26543a', normal, compile_fail, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/96bc4a6e5f7285e907e682705867b4fe... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/96bc4a6e5f7285e907e682705867b4fe... You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help