Skolem escape errors are not always reported as such
This program is correctly rejected, but with an unhelpful error message:
{-# LANGUAGE ExistentialQuantification #-}
module SK where
data Bar = forall a. Bar a
foo :: a -> ()
foo _ = ()
get :: Bar -> ()
get x = foo (case x of Bar a -> a)
SK.hs:10:33: error:
• Couldn't match expected type ‘a0’ with actual type ‘a’
‘a’ is a rigid type variable bound by
a pattern with constructor: Bar :: forall a. a -> Bar,
in a case alternative
at SK.hs:10:24-28
• In the expression: a
In a case alternative: Bar a -> a
In the first argument of ‘foo’, namely ‘(case x of { Bar a -> a })’
• Relevant bindings include
a :: a (bound at SK.hs:10:28)
|
10 | get x = foo (case x of Bar a -> a)
| ^
The root cause of the problem is an escaped skolem, namely a
, but the error message does not actually say that anywhere, making it quite confusing. The a0
variable is clearly a unification variable, so it is not obvious why it isn’t allowed to unify with a
.
The root cause of this issue is twofold:
-
During typechecking, we end up with the unsolvable wanted equality
a_ane[ssk:1] ~# a0_anb[tau:0]
. The skolem will always be placed on the left, sinceswapOverTyVars
prefers to put deeper tyvar on the left (as justified byNote [Deeper level on the left]
and #15009 (closed)). -
But
mkTyVarEqErr'
incorrectly assumes that if a skolem is on the left, a meta tyvar won’t ever be on the right. This assumption is outdated since 2bbdd00c, which first landed in GHC 8.6.
The culprit here appears to be mkTyVarEqErr'
, which should probably be modified to flip the equality around on its own if the left side is a skolem and the right side is a meta tyvar. Here’s a patch that does exactly that:
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index ae08f78443..8729de501f 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -1485,10 +1485,14 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 }
mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
+ | isUserSkolem ctxt tv1 -- if tv1 is a skolem and ty2 is a meta-tyvar,
+ , Just tv2 <- tcGetTyVar_maybe ty2 -- flip the equality around so that we
+ , isMetaTyVar tv2 -- report skolem escape errors (see #18114)
+ = mkTyVarEqErr' dflags ctxt report ct (flipSwap <$> oriented) tv2 ty1
+
| not insoluble_occurs_check -- See Note [Occurs check wins]
- , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
- -- be oriented the other way round;
- -- see GHC.Tc.Solver.Canonical.canEqTyVarTyVar
+ , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else we would have
+ -- flipped it around in the previous case
|| isTyVarTyVar tv1 && not (isTyVarTy ty2)
|| ctEqRel ct == ReprEq
-- the cases below don't really apply to ReprEq (except occurs check)
This appears to fix the issue, yielding a much nicer error message on the above program:
SK.hs:10:33: error:
• Couldn't match expected type ‘a0’ with actual type ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a pattern with constructor: Bar :: forall a. a -> Bar,
in a case alternative
at SK.hs:10:24-28
• In the expression: a
In a case alternative: Bar a -> a
In the first argument of ‘foo’, namely ‘(case x of { Bar a -> a })’
• Relevant bindings include
a :: a (bound at SK.hs:10:28)
|
10 | get x = foo (case x of Bar a -> a)
| ^
It needs a test case, but unless anyone has any objections, I intend to open an MR with the above patch soon.