Use tcView, not coreView, in the pure unifier.

Addresses a lingering point within #11715.

2 files changed, 24 insertions, 3 deletions

diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 3c6114ebd5..4c9bc19a7d 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -358,10 +358,28 @@ But in Core these two are treated as identical.
 
 We implement this by making 'coreView' convert 'Constraint' to 'TYPE
 LiftedRep' on the fly.  The function tcView (used in the type checker)
-does not do this.
+does not do this. Accordingly, tcView is used in type-checker-oriented
+functions (including the pure unifier, used in instance resolution),
+while coreView is used during e.g. optimisation passes.
 
 See also #11715, which tracks removing this inconsistency.
 
+The inconsistency actually leads to a potential soundness bug, in that
+Constraint and Type are considered *apart* by the type family engine.
+To wit, we can write
+
+  type family F a
+  type instance F Type = Bool
+  type instance F Constraint = Int
+
+and (because Type ~# Constraint in Core), thus build a coercion between
+Int and Bool. I (Richard E) conjecture that this never happens in practice,
+but it's very uncomfortable. This, essentially, is the root problem
+underneath #11715, which is quite resistant to an easy fix. The best
+idea is to have roles in kind coercions, but that has yet to be implemented.
+See also "A Role for Dependent Types in Haskell", ICFP 2019, which describes
+how roles in kinds might work out.
+
 -}
 
 -- | Gives the typechecker view of a type. This unwraps synonyms but
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index ed317da470..37b30629d5 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -957,7 +957,7 @@ unify_ty :: UMEnv
 -- Respects newtypes, PredTypes
 
 unify_ty env ty1 ty2 kco
-    -- TODO: More commentary needed here
+    -- Use tcView, not coreView. See Note [coreView vs tcView] in GHC.Core.Type.
   | Just ty1' <- tcView ty1   = unify_ty env ty1' ty2 kco
   | Just ty2' <- tcView ty2   = unify_ty env ty1 ty2' kco
   | CastTy ty1' co <- ty1     = if um_unif env
@@ -1121,7 +1121,8 @@ uUnrefined :: UMEnv
 -- We know that tv1 isn't refined
 
 uUnrefined env tv1' ty2 ty2' kco
-  | Just ty2'' <- coreView ty2'
+    -- Use tcView, not coreView. See Note [coreView vs tcView] in GHC.Core.Type.
+  | Just ty2'' <- tcView ty2'
   = uUnrefined env tv1' ty2 ty2'' kco    -- Unwrap synonyms
                 -- This is essential, in case we have
                 --      type Foo a = a
@@ -1412,6 +1413,8 @@ ty_co_match :: MatchEnv   -- ^ ambient helpful info
             -> Maybe LiftCoEnv
 ty_co_match menv subst ty co lkco rkco
   | Just ty' <- coreView ty = ty_co_match menv subst ty' co lkco rkco
+     -- why coreView here, not tcView? Because we're firmly after type-checking.
+     -- This function is used only during coercion optimisation.
 
   -- handle Refl case:
   | tyCoVarsOfType ty `isNotInDomainOf` subst