[Git][ghc/ghc][wip/T11715-2020] Use tcView, not coreView, in the pure unifier.

[Richard Eisenberg]

Richard Eisenberg pushed to branch wip/T11715-2020 at Glasgow Haskell Compiler / GHC


Commits:
dfdf0fc3 by Richard Eisenberg at 2020-08-05T12:26:18-04:00
Use tcView, not coreView, in the pure unifier.

Addresses a lingering point within #11715.

- - - - -


2 changed files:

- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs


Changes:

=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -357,10 +357,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


=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1121,7 +1121,7 @@ uUnrefined :: UMEnv
 -- We know that tv1 isn't refined
 
 uUnrefined env tv1' ty2 ty2' kco
-  | Just ty2'' <- coreView ty2'
+  | Just ty2'' <- tcView ty2'
   = uUnrefined env tv1' ty2 ty2'' kco    -- Unwrap synonyms
                 -- This is essential, in case we have
                 --      type Foo a = a
@@ -1483,6 +1483,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



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/dfdf0fc3fffbdfe40f94b12740349666bcd8c4fc
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/20200805/4bef2c00/attachment-0001.html>