[GHC] #15589: Always promoting metavariables during type inference may be wrong

[GHC]

#15589: Always promoting metavariables during type inference may be wrong
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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

 {{{#!hs
 {-# 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), 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
 [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs
 my thesis] -- section 6.5 to be specific.)

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15589>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler