Confusing interaction of pattern synonyms and view patterns
Summary
I'm using the bug report template, but I'm not entirely convinced it's a bug. Anyway.
This code rather surprisingly fails to compile:
{-# LANGUAGE PatternSynonyms, GADTs, ViewPatterns #-}
import Data.Typeable
data Gadt x y where
ExistentialInGadt :: Typeable a => a -> Gadt x x
pattern CastGadt :: Typeable a => x ~ y => a -> Gadt x y
pattern CastGadt a <- ExistentialInGadt (cast -> Just a)
test :: Gadt i o -> Bool
test gadt = case gadt of
CastGadt a -> a
_ -> False
The complete error message says:
test.hs:13:3: error:
• No instance for (Typeable a0) arising from a pattern
• In the pattern: CastGadt a
In a case alternative: CastGadt a -> a
In the expression:
case gadt of
CastGadt a -> a
_ -> False
|
13 | CastGadt a -> a
| ^^^^^^^^^^
test.hs:13:17: error:
• Couldn't match expected type ‘Bool’ with actual type ‘a0’
‘a0’ is untouchable
inside the constraints: i ~ o
bound by a pattern with pattern synonym:
CastGadt :: forall a x y. Typeable a => (x ~ y) => a -> Gadt x y,
in a case alternative
at test.hs:13:3-12
• In the expression: a
In a case alternative: CastGadt a -> a
In the expression:
case gadt of
CastGadt a -> a
_ -> False
• Relevant bindings include a :: a0 (bound at test.hs:13:12)
|
13 | CastGadt a -> a
| ^
Note that Typeable
isn't particularly relevant here, and neither are GADTs
, those are used for illustrative purposes -- the crux of the issue is given constraints on a pattern synonym using a view pattern that needs the required constraints.
It's not obvious why GHC insists a0
is untouchable. What's even more confusing, a pattern synonym without given constraints works as expected (i.e. it doesn't provide the constraint x ~ y
, but it does compile):
-- this compiles fine
pattern CastGadtNoGivens :: Typeable a => a -> Gadt x y
pattern CastGadtNoGivens a <- ExistentialInGadt (cast -> Just a)
test :: Gadt i o -> Bool
test gadt = case gadt of
CastGadtNoGivens a -> a
_ -> False
-- as expected, this would fail:
-- testGivens :: Gadt i o -> (i ~ o => Bool -> r) -> r
-- testGivens gadt f = case gadt of
-- CastGadtNoGivens x -> f x
Furthermore, the code substituting the pattern synonym definition compiles just fine, but that's not really a surprise:
-- This is totally fine
{-# LANGUAGE GADTs, ViewPatterns, TypeOperators #-}
import Data.Typeable
import Data.Type.Equality
data Gadt x y where
ExistentialInGadt :: Typeable a => a -> Gadt x x
test :: Gadt i o -> (Bool, i :~: o)
test gadt = case gadt of
ExistentialInGadt (cast -> Just a) -> (a, Refl)
_ -> undefined
Now, thanks to @int-index being very generous with his time, we more or less figured out why this happens. Specifically, in GHC.Tc.Gen.Pat.tcPatSynPat
we have:
; (ev_binds, (arg_pats', res))
<- checkConstraints skol_info ex_tvs' prov_dicts' $
tcConArgs (PatSynCon pat_syn) arg_tys_scaled tenv penv arg_pats thing_inside
All seems reasonable enough, however with the pattern synonym above, we run into a bit of an issue: checkConstraints
wants to know if a
is Typeable
to construct an implication, however it didn't actually typecheck the constructor arguments yet, as tcConArgs
is to be run later. Hence, it can't know yet what a
is and whether it's Typeable
.
The pattern synonym without givens apparently works because checkConstraints
goes into the "fast path" and actually skips building the implications.
I didn't really investigate the code without pattern synonyms, but my hunch is cast
is applied before givens are brought into scope (semantically this makes sense at least).
#19847 (closed) and #21501 (closed) seem to be symptoms of this very same issue (to be clear: I didn't run traces, but the setup is the same), but those also use pattern type applications, and that complicates things a bit.
Steps to reproduce
Copy the code above and try to compile it (or load it in GHCi)
Expected behavior
The code compiles, or at least a less arcane error message is produced.
Environment
- GHC version used: 9.0, 9.2, 9.4