[Git][ghc/ghc][wip/T23070-unify] Fix a boo boo

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T23070-unify at Glasgow Haskell Compiler / GHC


Commits:
8a07526c by Simon Peyton Jones at 2023-04-02T22:21:29+01:00
Fix a boo boo

- - - - -


1 changed file:

- compiler/GHC/Tc/Utils/Unify.hs


Changes:

=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1805,7 +1805,8 @@ uType_defer (UE { u_loc = loc, u_defer = ref, u_role = role })
        ; whenDOptM Opt_D_dump_tc_trace $
          do { ctxt <- getErrCtxt
             ; doc  <- mkErrInfo emptyTidyEnv ctxt
-            ; traceTc "utype_defer" (vcat [ debugPprType ty1
+            ; traceTc "utype_defer" (vcat [ ppr role
+                                          , debugPprType ty1
                                           , debugPprType ty2
                                           , doc])
             ; traceTc "utype_defer2" (ppr co) }
@@ -1824,7 +1825,7 @@ uType env@(UE { u_role = role }) orig_ty1 orig_ty2
   = do { tclvl <- getTcLevel
        ; traceTc "u_tys" $ vcat
               [ text "tclvl" <+> ppr tclvl
-              , sep [ ppr orig_ty1, text "~", ppr orig_ty2] ]
+              , sep [ ppr orig_ty1, text "~" <> ppr role, ppr orig_ty2] ]
        ; co <- go orig_ty1 orig_ty2
        ; if isReflCo co
             then traceTc "u_tys yields no coercion" Outputable.empty
@@ -1854,14 +1855,15 @@ uType env@(UE { u_role = role }) orig_ty1 orig_ty2
       = do { lookup_res <- isFilledMetaTyVar_maybe tv1
            ; case lookup_res of
                Just ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
-                                ; go ty1 ty2 }
-               Nothing  -> uUnfilledVar env NotSwapped tv1 ty2 }
+                              ; uType env ty1 orig_ty2 }
+               Nothing -> uUnfilledVar env NotSwapped tv1 ty2 }
+
     go ty1 (TyVarTy tv2)
       = do { lookup_res <- isFilledMetaTyVar_maybe tv2
            ; case lookup_res of
                Just ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
-                              ; go ty1 ty2 }
-               Nothing  -> uUnfilledVar env IsSwapped tv2 ty1 }
+                              ; uType env orig_ty1 ty2 }
+               Nothing -> uUnfilledVar env IsSwapped tv2 ty1 }
 
       -- See Note [Expanding synonyms during unification]
     go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
@@ -1941,7 +1943,7 @@ uType env@(UE { u_role = role }) orig_ty1 orig_ty2
     ------------------
     defer ty1 ty2   -- See Note [Check for equality before deferring]
       | ty1 `tcEqType` ty2 = return (mkReflCo role ty1)
-      | otherwise          = uType_defer env ty1 ty2
+      | otherwise          = uType_defer env orig_ty1 orig_ty2
 
 
     ------------------
@@ -2066,15 +2068,23 @@ uUnfilledVar, uUnfilledVar1
     -> TcM CoercionN
 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
 --            It might be a skolem, or untouchable, or meta
-
+--
+-- Precondition: u_role env = Nominal
 uUnfilledVar env swapped tv1 ty2
-  = do { ty2 <- zonkTcType ty2    -- Zonk to expose things to the
-                                  -- occurs check, and so that if ty2
-                                  -- looks like a type variable then it
+  | Nominal <- u_role env
+  = do { ty2 <- zonkTcType ty2    -- Zonk to expose things to the occurs check, and so
+                                  -- that if ty2 looks like a type variable then it
                                   -- /is/ a type variable
        ; uUnfilledVar1 env swapped tv1 ty2 }
 
-uUnfilledVar1 env@(UE { u_role = role }) swapped tv1 ty2  -- ty2 is zonked
+  | otherwise  -- See Note [Do not unify representational equalities]
+               -- in GHC.Tc.Solver.Equality
+  = unSwap swapped (uType_defer env) (mkTyVarTy tv1) ty2
+
+uUnfilledVar1 env       -- u_role==Nominal
+              swapped
+              tv1
+              ty2       -- ty2 is zonked
   | Just tv2 <- getTyVar_maybe ty2
   = go tv2
 
@@ -2086,7 +2096,7 @@ uUnfilledVar1 env@(UE { u_role = role }) swapped tv1 ty2  -- ty2 is zonked
     -- tyvars so we might want to swap
     -- E.g. maybe tv2 is a meta-tyvar and tv1 is not
     go tv2 | tv1 == tv2  -- Same type variable => no-op
-           = return (mkReflCo role (mkTyVarTy tv1))
+           = return (mkNomReflCo (mkTyVarTy tv1))
 
            | swapOverTyVars False tv1 tv2   -- Distinct type variables
                -- Swap meta tyvar to the left if poss
@@ -2107,7 +2117,7 @@ uUnfilledVar2 :: UnifyEnv
                                 --    definitely not a /filled/ meta-tyvar
               -> TcTauType      -- Type 2, zonked
               -> TcM CoercionN
-uUnfilledVar2 env@(UE { u_role = role }) swapped tv1 ty2
+uUnfilledVar2 env swapped tv1 ty2
   = do { cur_lvl <- getTcLevel
            -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
            -- Here we don't know about given equalities here; so we treat
@@ -2127,7 +2137,7 @@ uUnfilledVar2 env@(UE { u_role = role }) swapped tv1 ty2
            -- NB: tv1 should still be unfilled, despite the kind unification
            --     because tv1 is not free in ty2' (or, hence, in its kind)
          then do { writeMetaTyVar tv1 ty2
-                 ; return (mkReflCo role ty2) }
+                 ; return (mkNomReflCo ty2) }
 
          else defer  -- This cannot be solved now.  See GHC.Tc.Solver.Canonical
                      -- Note [Equalities with incompatible kinds] for how



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8a07526caf34c77e528c805eeed918a693fdaac6
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/20230402/6ca506c8/attachment-0001.html>