Always promoting metavariables during type inference may be wrong

Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.

Consider

{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
             AllowAmbiguousTypes #-}

import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind

data SameKind :: forall k. k -> k -> Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
   IfK (_ :: Proxy True)  f _ = f
   IfK (_ :: Proxy False) _ g = g

y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True -> ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
             x = undefined
         in ()

This panics currently (#15588 (closed)), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.

• We can derive IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j -> m -> n -> If j m n, where If :: forall k. Bool -> k -> k -> k is imported from Data.Type.Bool and is a straightforward conditional choice operator.
• In the type of x, we see that we need the kind of IfK c b d to match the kind of d. That is, if b :: kappa[3], we have [W] If cb kappa[3] a ~ a. Here, the forall in x's type is at level 3; the RHS of y is at level 2.
• If we could reduce If cb kappa[3] a to kappa[3], then we would solve kappa[3] := a, but we can't make this reduction, because cb is a skolem.
• Instead, we finish checking the type of x and promote kappa[3] to kappa[2].
• Later, we'll make an implication constraint with [G] cb ~ True. When solving that implication constraint, we'll get [W] If True kappa[2] a ~ a and simplify to [W] kappa[2] ~ a, but that will be insoluble because we'll be solving at level 3, and now kappa[2] is at level 2. We're too late.

Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know cb ~ True the first time we try to solve, and then we'll succeed.

An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case -- promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in my thesis -- section 6.5 to be specific.)

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture