Typed Holes, GADTs and residual constraints
Opened this issue · 3 comments
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).
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)
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
tof :: (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 bindingx :: Expr a
, but not to the bindingfoo :: Expr a -> Bool
. (Btw, does this qualify as a bug? The typed hole seems to suggest thatfoo
can only be used at typeExpr Bool -> Bool
, while it can actually be used at typeforall a. Expr a -> Bool
.)
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
...