[Git][ghc/ghc][wip/int-index/visibility-subsumption] WIP: Visibility checks in qlUnify and checkTypeEq
Vladislav Zavialov (@int-index)
gitlab at gitlab.haskell.org
Thu Feb 2 10:52:56 UTC 2023
Vladislav Zavialov pushed to branch wip/int-index/visibility-subsumption at Glasgow Haskell Compiler / GHC
Commits:
3aadd24f by Vladislav Zavialov at 2023-02-02T13:52:32+03:00
WIP: Visibility checks in qlUnify and checkTypeEq
- - - - -
10 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/typecheck/should_fail/T15079_fail_b.stderr
- + testsuite/tests/typecheck/should_fail/T22648v.hs
- + testsuite/tests/typecheck/should_fail/T22648v.stderr
- + testsuite/tests/typecheck/should_fail/T22648v_ql.hs
- + testsuite/tests/typecheck/should_fail/T22648v_ql.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -1054,7 +1054,7 @@ qlUnify delta ty1 ty2
kappa_kind = tyVarKind kappa
; co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
-- unifyKind: see Note [Actual unification in qlUnify]
-
+ ; checkSubVis ty2_kind (Check kappa_kind)
; traceTc "qlUnify:update" $
vcat [ hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -34,6 +34,7 @@ module GHC.Tc.Types.Constraint (
CheckTyEqResult, CheckTyEqProblem, cteProblem, cterClearOccursCheck,
cteOK, cteImpredicative, cteTypeFamily,
cteInsolubleOccurs, cteSolubleOccurs, cterSetOccursCheckSoluble,
+ cteForallVisDiff,
cterHasNoProblem, cterHasProblem, cterHasOnlyProblem,
cterRemoveProblem, cterHasOccursCheck, cterFromKind,
@@ -452,12 +453,13 @@ cterHasNoProblem _ = False
-- | An individual problem that might be logged in a 'CheckTyEqResult'
newtype CheckTyEqProblem = CTEP Word8
-cteImpredicative, cteTypeFamily, cteInsolubleOccurs, cteSolubleOccurs :: CheckTyEqProblem
+cteImpredicative, cteTypeFamily, cteInsolubleOccurs, cteSolubleOccurs, cteForallVisDiff :: CheckTyEqProblem
cteImpredicative = CTEP (bit 0) -- forall or (=>) encountered
cteTypeFamily = CTEP (bit 1) -- type family encountered
cteInsolubleOccurs = CTEP (bit 2) -- occurs-check
cteSolubleOccurs = CTEP (bit 3) -- occurs-check under a type function or in a coercion
-- must be one bit to the left of cteInsolubleOccurs
+cteForallVisDiff = CTEP (bit 4) -- differing visibility of forall-bound variables
-- See also Note [Insoluble occurs check] in GHC.Tc.Errors
cteProblem :: CheckTyEqProblem -> CheckTyEqResult
@@ -521,7 +523,8 @@ instance Outputable CheckTyEqResult where
all_bits = [ (cteImpredicative, "cteImpredicative")
, (cteTypeFamily, "cteTypeFamily")
, (cteInsolubleOccurs, "cteInsolubleOccurs")
- , (cteSolubleOccurs, "cteSolubleOccurs") ]
+ , (cteSolubleOccurs, "cteSolubleOccurs")
+ , (cteForallVisDiff, "cteForallVisDiff") ]
set_bits = [ text str
| (bitmask, str) <- all_bits
, cter `cterHasProblem` bitmask ]
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -68,7 +68,7 @@ module GHC.Tc.Utils.TcMType (
--------------------------------
-- Visibility subsumption
- tcSubVis, checkSubVis,
+ tcSubVis, tcEqVis, checkSubVis,
--------------------------------
-- Zonking and tidying
@@ -620,6 +620,13 @@ checkSubVis ty1 (Check ty2) =
unless (tcSubVis ty1 ty2) $
addErr $ TcRnIncompatibleForallVisibility ty1 ty2
+tcEqVis :: Type -> Type -> Bool
+tcEqVis ty1 ty2 =
+ Semi.getAll (zipForAllTyFlags eq_vis ty1 ty2)
+ where
+ eq_vis :: ForAllTyFlag -> ForAllTyFlag -> Semi.All
+ eq_vis flag1 flag2 = Semi.All (flag1 == flag2)
+
tcSubVis
:: Type -- actual
-> Type -- expected
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2637,12 +2637,13 @@ checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult
-- case-analysis on 'lhs')
-- * checkEqCanLHSFinish, which does not know the form of 'lhs'
checkTypeEq lhs ty
- = go ty
+ = go ty S.<> check_kind_vis (canEqLHSKind lhs) (typeKind ty)
where
impredicative = cteProblem cteImpredicative
type_family = cteProblem cteTypeFamily
insoluble_occurs = cteProblem cteInsolubleOccurs
soluble_occurs = cteProblem cteSolubleOccurs
+ forall_vis_diff = cteProblem cteForallVisDiff
-- The GHCi runtime debugger does its type-matching with
-- unification variables that can unify with a polytype
@@ -2722,3 +2723,8 @@ checkTypeEq lhs ty
| ghci_tv = \ _tc -> cteOK
| otherwise = \ tc -> (if isTauTyCon tc then cteOK else impredicative) S.<>
(if isFamFreeTyCon tc then cteOK else type_family)
+
+ check_kind_vis :: TcKind -> TcKind -> CheckTyEqResult
+ check_kind_vis k1 k2
+ | tcEqVis k1 k2 = cteOK
+ | otherwise = forall_vis_diff
=====================================
testsuite/tests/typecheck/should_fail/T15079_fail_b.stderr
=====================================
@@ -1,8 +1,8 @@
-T15079_fail_b.hs:21:23: error: [GHC-25115]
- • Visibility of forall-bound variables is not compatible
- Expected: forall i. i -> *
- Actual: forall {k}. k -> *
+T15079_fail_b.hs:21:23: error: [GHC-83865]
+ • Couldn't match type ‘c0’ with ‘Coerce’
+ Expected: c0 a -> Coerce b
+ Actual: c0 a -> c0 b
• In the first argument of ‘(.)’, namely ‘hsubst f’
In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’
In the expression: uncoerce . hsubst f . Coerce
=====================================
testsuite/tests/typecheck/should_fail/T22648v.hs
=====================================
@@ -0,0 +1,18 @@
+module T22648v where
+
+import Data.Kind (Type)
+
+type V :: forall k -> k -> Type
+data V k (a :: k) = MkV
+
+f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
+f _ = ()
+
+bad_tyapp :: ()
+bad_tyapp = f @V MkV
+
+bad_wild :: ()
+bad_wild = f @_ MkV
+
+bad_infer :: ()
+bad_infer = f MkV
=====================================
testsuite/tests/typecheck/should_fail/T22648v.stderr
=====================================
@@ -0,0 +1,23 @@
+
+T22648v.hs:12:16: error: [GHC-25115]
+ • Visibility of forall-bound variables is not compatible
+ Expected: forall j. j -> *
+ Actual: forall k -> k -> *
+ • In the type ‘V’
+ In the expression: f @V MkV
+ In an equation for ‘bad_tyapp’: bad_tyapp = f @V MkV
+
+T22648v.hs:15:15: error: [GHC-91028]
+ • Expected kind ‘forall j. j -> *’, but ‘_’ has kind ‘k0’
+ Cannot instantiate unification variable ‘k0’
+ with a kind involving polytypes: forall j. j -> *
+ • In the expression: f @_ MkV
+ In an equation for ‘bad_wild’: bad_wild = f @_ MkV
+
+T22648v.hs:18:15: error: [GHC-83865]
+ • Couldn't match type ‘hk0’ with ‘V’
+ Expected: hk0 a0
+ Actual: V k1 a0
+ • In the first argument of ‘f’, namely ‘MkV’
+ In the expression: f MkV
+ In an equation for ‘bad_infer’: bad_infer = f MkV
=====================================
testsuite/tests/typecheck/should_fail/T22648v_ql.hs
=====================================
@@ -0,0 +1,20 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module T22648v_ql where
+
+import Data.Kind (Type)
+
+type V :: forall k -> k -> Type
+data V k (a :: k) = MkV
+
+f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
+f _ = ()
+
+bad_tyapp :: ()
+bad_tyapp = f @V MkV
+
+bad_wild :: ()
+bad_wild = f @_ MkV
+
+bad_infer :: ()
+bad_infer = f MkV
=====================================
testsuite/tests/typecheck/should_fail/T22648v_ql.stderr
=====================================
@@ -0,0 +1,23 @@
+
+T22648v_ql.hs:14:16: error: [GHC-25115]
+ • Visibility of forall-bound variables is not compatible
+ Expected: forall j. j -> *
+ Actual: forall k -> k -> *
+ • In the type ‘V’
+ In the expression: f @V MkV
+ In an equation for ‘bad_tyapp’: bad_tyapp = f @V MkV
+
+T22648v_ql.hs:17:15: error: [GHC-91028]
+ • Expected kind ‘forall j. j -> *’, but ‘_’ has kind ‘k0’
+ Cannot instantiate unification variable ‘k0’
+ with a kind involving polytypes: forall j. j -> *
+ • In the expression: f @_ MkV
+ In an equation for ‘bad_wild’: bad_wild = f @_ MkV
+
+T22648v_ql.hs:20:15: error: [GHC-25115]
+ • Visibility of forall-bound variables is not compatible
+ Expected: forall j. j -> *
+ Actual: forall k -> k -> *
+ • In the first argument of ‘f’, namely ‘MkV’
+ In the expression: f MkV
+ In an equation for ‘bad_infer’: bad_infer = f MkV
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -669,5 +669,7 @@ test('T20666', normal, compile_fail, [''])
test('T20666a', normal, compile_fail, [''])
test('T22648a', normal, compile_fail, [''])
test('T22648b', normal, compile_fail, [''])
+test('T22648v', normal, compile_fail, [''])
+test('T22648v_ql', normal, compile_fail, [''])
test('T15079_fail_a', normal, compile_fail, [''])
test('T15079_fail_b', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3aadd24f5d3117e901c94b334b5976e611291b7f
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3aadd24f5d3117e901c94b334b5976e611291b7f
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/20230202/2e278282/attachment-0001.html>
More information about the ghc-commits
mailing list