[Git][ghc/ghc][wip/T24676] Instantiation variables can leak into the constraint solver, just

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC


Commits:
6d024220 by Simon Peyton Jones at 2024-06-04T15:16:26+01:00
Instantiation variables can leak into the constraint solver, just

- - - - -


3 changed files:

- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Solver/Equality.hs
- testsuite/tests/typecheck/should_fail/VisFlag1_ql.stderr


Changes:

=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -123,7 +123,8 @@ Note [Instantiation variables are short lived]
 
   See Section 4.3 "Applications and instantiation" of the paper.
 
-* The constraint solver never sees an instantiation variable.
+* The constraint solver never sees an instantiation variable [not quite true;
+  see below]
 
   However, the constraint solver can see a meta-type-variable filled
   in with a polytype (#18987). Suppose
@@ -145,6 +146,21 @@ Note [Instantiation variables are short lived]
   Since the constraint solver does not do implicit instantiation (as the
   constraint generator does), the fact that a unification variable might stand
   for a polytype does not matter.
+
+* Actually, sadly the constraint solver /can/ see an instantiation variable.
+  Consider this from test VisFlag1_ql:
+     f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
+
+     bad_wild :: ()
+     bad_wild = f @_ MkV
+  In tcInstFun instantiate f with [k:=k0, a:=a0], and then encounter the `@_`,
+  expecting it to have kind (forall j. j->Type).  We make a fresh variable (it'll
+  be an instantiation variable since we are in tcInstFun) for the `_`, thus
+  (_ : k0) and do `checkExpectedKind` to match up `k0` with `forall j. j->Type`.
+  The unifier doesn't solve it (it does not unify instantiation variables) so
+  it leaves it for the constraint solver.  Yuk.   It's hard to see what to do
+  about this, but it seems to do no harm for the constraint solver to see the
+  occasional instantiation variable.
 -}
 
 


=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1821,9 +1821,6 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
               , text "lhs:" <+> ppr lhs
               , text "rhs:" <+> ppr rhs ]
 
-         -- Assertion: no QL instantiation tyvars
-       ; massertPpr (not (ql_inst_tv lhs)) (ppr lhs)
-
          -- Assertion: (TyEq:K) is already satisfied
        ; massert (canEqLHSKind lhs `eqType` typeKind rhs)
 
@@ -1835,9 +1832,6 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
        ; canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs }
 
   where
-    ql_inst_tv (TyVarLHS tv) = isQLInstTyVar tv
-    ql_inst_tv (TyFamLHS {}) = False
-
     -- This is about (TyEq:N): check that we don't have a saturated application
     -- of a newtype TyCon at the top level of the RHS, if the constructor
     -- of the newtype is in scope.


=====================================
testsuite/tests/typecheck/should_fail/VisFlag1_ql.stderr
=====================================
@@ -6,12 +6,11 @@ VisFlag1_ql.hs:14:16: error: [GHC-83865]
       In the expression: f @V MkV
       In an equation for ‘bad_tyapp’: bad_tyapp = f @V MkV
 
-VisFlag1_ql.hs:17:17: error: [GHC-83865]
-    • Expecting one more argument to ‘V’
-      Expected kind ‘forall j. j -> *’,
-        but ‘V’ has kind ‘forall k -> k -> *’
-    • In the second argument of ‘f’, namely ‘MkV’
-      In the expression: f @_ MkV
+VisFlag1_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
 
 VisFlag1_ql.hs:20:15: error: [GHC-83865]



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6d0242204ede318af23ff74b324b3399a6ec5415

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6d0242204ede318af23ff74b324b3399a6ec5415
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/20240604/76085603/attachment-0001.html>