[Git][ghc/ghc][wip/T24676] Emit an equality constraint in make_kinds_ok

[Simon Peyton Jones (@simonpj)]

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


Commits:
f4ccf0cd by Simon Peyton Jones at 2024-05-20T17:34:31+01:00
Emit an equality constraint in make_kinds_ok

Makes QL a tiny bit more robust

Consider:
  k :: Type
  co :: k ~ Type
  f :: forall (a :: k). Proxy k a -> blah
  q :: Proxy Type (forall b. b -> b)
  x = ... f q ...

When QL-ing (f q) we'll instantiate `a` with `kappa` and qlUnify
  Proxy k kappa ~ Proxy Type (forall b. b->b)

Ql-Unifying k with Type will fail; fine.
If ql-unifying (kappa::k) with (forall b. b->b) fails, then kappa will
end up as a mono-tyvar and subsequent unification will fail. But it
can succed with (kappa := (forall b. b->b) |> co), where we emit
an equalityconstraint for `co`.

- - - - -


1 changed file:

- compiler/GHC/Tc/Gen/App.hs


Changes:

=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -21,11 +21,9 @@ module GHC.Tc.Gen.App
 
 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )
 
-import GHC.Types.Var
-import GHC.Builtin.Types ( multiplicityTy )
-import GHC.Tc.Gen.Head
-import Language.Haskell.Syntax.Basic
 import GHC.Hs
+
+import GHC.Tc.Gen.Head
 import GHC.Tc.Errors.Types
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Unify
@@ -38,6 +36,7 @@ import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.TcType as TcType
 import GHC.Tc.Zonk.TcType
+
 import GHC.Core.ConLike (ConLike(..))
 import GHC.Core.DataCon (dataConConcreteTyVars)
 import GHC.Core.TyCon
@@ -47,20 +46,29 @@ import GHC.Core.TyCo.Subst (substTyWithInScope)
 import GHC.Core.TyCo.FVs
 import GHC.Core.Type
 import GHC.Core.Coercion
-import GHC.Types.Var.Set
+
+import GHC.Builtin.Types ( multiplicityTy )
 import GHC.Builtin.PrimOps( tagToEnumKey )
 import GHC.Builtin.Names
 import GHC.Driver.DynFlags
+
+import GHC.Types.Var
 import GHC.Types.Name
 import GHC.Types.Name.Env
 import GHC.Types.Name.Reader
 import GHC.Types.SrcLoc
+import GHC.Types.Var.Set
 import GHC.Types.Var.Env  ( emptyTidyEnv, mkInScopeSet )
+import GHC.Types.Basic( TypeOrKind(..) )
+
 import GHC.Data.Maybe
+
 import GHC.Utils.Misc
 import GHC.Utils.Outputable as Outputable
 import GHC.Utils.Panic
+
 import qualified GHC.LanguageExtensions as LangExt
+import Language.Haskell.Syntax.Basic
 
 import Control.Monad
 import Data.Function
@@ -1882,29 +1890,43 @@ qlUnify delta ty1 ty2
           -- Passes the occurs check
       , not (isConcreteTyVar kappa) || isConcreteType ty2
           -- Don't unify a concrete instantiatiation variable with a non-concrete type
-      = do { let kappa_kind = tyVarKind kappa
-                 ty2_kind   = typeKind ty2
-           ; kinds_ok <- go_kinds kappa_kind ty2_kind
-           ; when kinds_ok $  -- If kinds_ok is False, we simply no-op
-                -- See Note [Actual unification during QuickLook] (UQL2)
-             do { traceTc "qlUnify:update" $
-                  hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
-                     2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
-                ; liftZonkM $ writeMetaTyVar kappa ty2 }}
+      = do { ty2' <- make_kinds_ok kappa ty2
+           ; traceTc "qlUnify:update" $
+             ppr kappa <+> text ":=" <+> ppr ty2
+           ; liftZonkM $ writeMetaTyVar kappa ty2' }
 
       | otherwise
       = return ()   -- Occurs-check or forall-bound variable
 
-    go_kinds :: TcKind -> TcKind -> TcM Bool
+    make_kinds_ok :: TcTyVar -> TcType -> TcM TcType
+    -- Don't call unifyKind!  Instead try to make the kinds equal with
+    -- unifyKind; and if that fails just emit an equality
     -- See Note [Actual unification during QuickLook] (UQL2)
-    go_kinds kind1 kind2
-      | kind1 `tcEqType` kind2 = return True
-      | otherwise              = do { qlUnify delta kind1 kind2
-                                    ; liftZonkM $
-                                      do { kind1 <- zonkTcType kind1
-                                         ; kind2 <- zonkTcType kind2
-                                         ; return (kind1 `tcEqType` kind2) } }
-
+    make_kinds_ok kappa ty2
+      | kind1 `tcEqType` kind2
+      = return ty2
+      | otherwise
+      = do { qlUnify delta kind1 kind2
+           ; (kind1, kind2) <- liftZonkM $
+                               do { kind1 <- zonkTcType kind1
+                                  ; kind2 <- zonkTcType kind2
+                                  ; return (kind1, kind2) }
+           ; if (kind1 `tcEqType` kind2)
+             then return ty2
+             else
+        do { co <- emitWantedEq orig KindLevel Nominal kind1 kind2
+           ; traceTc "make_kinds_ok" $
+             vcat [ hang (ppr kappa <+> dcolon <+> ppr kind1 <+> text ":=")
+                       2 (ppr ty2 <+> dcolon <+> ppr kind2)
+                  , text "co:" <+> ppr co ]
+           ; return (mkCastTy ty2 co) } }
+      where
+        kind1 = tyVarKind kappa
+        kind2 = typeKind ty2
+        orig  = TypeEqOrigin { uo_actual   = kind1
+                             , uo_expected = kind2
+                             , uo_thing    = Just (TypeThing ty2)
+                             , uo_visible  = True }
 
 {- Note [Actual unification during QuickLook]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f4ccf0cdbd9ba531ce71726a8b37df584b929ebf
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/20240520/f7f90437/attachment-0001.html>