Typed Holes, GADTs and residual constraints

[BinderDavid]

The error messages when using typed holes on the RHS of a pattern match on GADT constructors are not optimal, since type equality constraints are left unresolved and not applied as substitutions. (Tested with GHC 8.6, 8.10 and 9.2.1). Understanding the error message requires understanding both GADTs and the implementation of GADTs with the help of type equality constraints.

Example

Consider the following snippet:

{-# LANGUAGE GADTs #-}

data Expr a where
  ExprInt :: Int -> Expr Int
  ExprBool :: Bool -> Expr Bool

foo :: Expr a -> Bool
foo x = case x of
  ExprInt _ -> True
  ExprBool _ -> _

The error message I get (shortened):

example.hs:10:17: error:
    • Found hole: _ :: Bool
    • In the expression: _
      In a case alternative: ExprBool _ -> _
      In the expression:
        case x of
          ExprInt _ -> True
          ExprBool _ -> _
    • Relevant bindings include
        x :: Expr a (bound at example.hs:8:5)
        foo :: Expr a -> Bool (bound at example.hs:8:1)
      Constraints include a ~ Bool (from example.hs:10:3-12)

This error message correctly identifies the constraint a ~ Bool which came into context by pattern matching on the GADT constructor ExprBool. But understanding this error message requires understanding how GADT constructors are desugared internally (into ExprBool :: forall a. a ~ Bool => Bool -> Expr a)

The error message I would ideally expect would turn this constraint into a substitution and apply it:

example.hs:10:17: error:
    • Found hole: _ :: Bool
    • In the expression: _
      In a case alternative: ExprBool _ -> _
      In the expression:
        case x of
          ExprInt _ -> True
          ExprBool _ -> _
    • Relevant bindings include
        x :: Expr Bool (bound at example.hs:8:5)
        foo :: Expr a -> Bool (bound at example.hs:8:1)

I am not very familiar with GHC internals, in particular how closely GHC follows the implementation described in the OutsideIn paper, but the problem is probably that a is considered an untouchable unification variable within the implication constraint generated for the RHS of the pattern match. But for the typed hole, the unification variable a should probably be allowed to unify with Bool. (Except for the occurrence in foo, of course).

[goldfirere]

Thanks for posting this! And thanks for including a concrete suggestion for improvement.

I agree that the new output is correct. Why do you think the new output is better? That is, I can't come up with a reason that applying the substitution leads to a better message than not applying it. Maybe thinking in terms of a is easier. Maybe the problem is that the error message is mixed? We have _ :: Bool at the top, but references to a elsewhere.

On the other hand, we might be able to do better in stating the constraint. Specifically, instead of

      Constraints include a ~ Bool (from example.hs:10:3-12)

we could have

      In this context, 'a' is known to be 'Bool' (from a GADT pattern match at example.hs:10:3-12)

[BinderDavid]

I agree that the new output is correct. Why do you think the new output is better? That is, I can't come up with a reason that applying the substitution leads to a better message than not applying it

Maybe it comes down to a question of preferences, but I will try to give my pseudo-objective reasons for prefering my suggested error message.

• When inferring types we usually try to solve constraints instead of leaving them unsolved. I.e. we prefer f :: Int -> Bool to f :: (a ~ Int, b ~ Bool) => a -> b. The unsolved constraints should only appear whenever it is not possible to solve/substitute them.
• When reading and interpreting the state of the typed hole, I have to mentally perform the substitution myself. (At least that is how I read that typed hole). I would prefer to have the compiler perform that substitution for me.
• It is possible to understand the typed hole even if you don't know about type equality constraints, and only about GADTs. But this last point would also be solved by your suggestion of phrasing the constraint differently.
• For the concrete example given above, it also solves the problem that the constraint a ~ Bool applies only to the binding x :: Expr a, but not to the binding foo :: Expr a -> Bool. (Btw, does this qualify as a bug? The typed hole seems to suggest that foo can only be used at type Expr Bool -> Bool, while it can actually be used at type forall a. Expr a -> Bool.)

[xplat]

Hm, this does seem like a bug since the type signature of foo makes polymorphic recursion possible in the hole; foo should be shown with either a renamed type variable or an explicit forall. Contrariwise, x can only be used at type Expr Bool or Expr a for the inherited a which is equal to Bool ...