Commit db8793ad authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot
Browse files

Use tcView, not coreView, in the pure unifier.

Addresses a lingering point within #11715.
parent 0a1ecc5f
......@@ -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
......@@ -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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment