[Git][ghc/ghc][wip/cfuneqcan-refactor] 2 commits: Revisit [Prevent unification with type families]

[Richard Eisenberg]

Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC


Commits:
f235a943 by Richard Eisenberg at 2020-11-12T17:29:20-05:00
Revisit [Prevent unification with type families]

- - - - -
7d26bf41 by Richard Eisenberg at 2020-11-13T11:15:53-05:00
Don't flatten during instance lookup

- - - - -


3 changed files:

- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Utils/Unify.hs


Changes:

=====================================
compiler/GHC/Core/InstEnv.hs
=====================================
@@ -41,7 +41,6 @@ import GHC.Unit.Types
 import GHC.Core.Class
 import GHC.Types.Var
 import GHC.Types.Var.Set
-import GHC.Types.Var.Env
 import GHC.Types.Name
 import GHC.Types.Name.Set
 import GHC.Types.Unique (getUnique)
@@ -836,13 +835,10 @@ lookupInstEnv' ie vis_mods cls tys
                 -- Unification will break badly if the variables overlap
                 -- They shouldn't because we allocate separate uniques for them
                 -- See Note [Template tyvars are fresh]
-        let in_scope      = mkInScopeSet (tpl_tv_set `unionVarSet` tys_tv_set)
-            flattened_tys = flattenTys in_scope tys in
-              -- NB: important to flatten here. Otherwise, it looks like
-              -- instance C Int cannot match a target [W] C (F Bool).
-              -- See Note [Flattening type-family applications when matching instances]
-              -- in GHC.Core.Unify.
-        case tcUnifyTysFG instanceBindFun tpl_tys flattened_tys of
+        case tcUnifyTysFG instanceBindFun tpl_tys tys of
+          -- We consider MaybeApart to be a case where the instance might
+          -- apply in the future. This covers an instance like C Int and
+          -- a target like [W] C (F a), where F is a type family.
             SurelyApart -> find ms us        rest
             _           -> find ms (item:us) rest
       where


=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1015,7 +1015,8 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
   | Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
   , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
    -- we want to catch e.g. Maybe Int ~ (Int -> Int) here for better
-   -- error messages; hence no direct match on TyConApp
+   -- error messages rather than decomposing into AppTys;
+   -- hence no direct match on TyConApp
   , not (isTypeFamilyTyCon tc1)
   , not (isTypeFamilyTyCon tc2)
   = canTyConApp ev eq_rel tc1 tys1 tc2 tys2


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1434,7 +1434,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
   where
     go dflags cur_lvl
       | canSolveByUnification cur_lvl tv1 ty2
-           -- See Note [Prevent unification with type families] about the False:
+           -- See Note [Prevent unification with type families] about the NoTypeFamilies:
       , MTVU_OK ty2' <- metaTyVarUpdateOK dflags NoTypeFamilies tv1 ty2
       = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1)
            ; traceTc "uUnfilledVar2 ok" $
@@ -1677,6 +1677,9 @@ It would be lovely in the future to revisit this problem and remove this
 extra, unnecessary check. But we retain it for now as it seems to work
 better in practice.
 
+Revisited in Nov '20, along with removing flattening variables. Problem
+is still present, and the solution (NoTypeFamilies) is still the same.
+
 Note [Refactoring hazard: metaTyVarUpdateOK]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 I (Richard E.) have a sad story about refactoring this code, retained here



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0b4d386cc779db18e9fdb266cf76bff341fb126a...7d26bf41f46bbbe9f1479fdb970d171f2f867326

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0b4d386cc779db18e9fdb266cf76bff341fb126a...7d26bf41f46bbbe9f1479fdb970d171f2f867326
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/20201113/5851a17e/attachment-0001.html>