Opened 7 months ago
Closed 7 months ago
#13441 closed bug (fixed)
Type inference failure in bidirectional pattern synonym and GADT pattern match
Reported by: | goldfire | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.2.1 |
Component: | Compiler | Version: | 8.1 |
Keywords: | PatternSynonyms | Cc: | Iceland_jack |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
In my musings in preparation toward teaching my undergrads about GADTs, I tried defining the usual old Vec
in terms of FList
s (definition below) and pattern synonyms. Here is the code:
{-# LANGUAGE ScopedTypeVariables, PatternSynonyms, DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies #-} module VecFList where import Data.Functor.Identity data FList f xs where FNil :: FList f '[] (:@) :: f x -> FList f xs -> FList f (x ': xs) data Nat = Zero | Succ Nat type family Length (xs :: [k]) :: Nat where Length '[] = Zero Length (_ ': xs) = Succ (Length xs) type family Replicate (n :: Nat) (x :: a) = (r :: [a]) where Replicate Zero _ = '[] Replicate (Succ n) x = x ': Replicate n x type Vec n a = FList Identity (Replicate n a) pattern Nil :: forall n a. n ~ Length (Replicate n a) => n ~ Zero => Vec n a pattern Nil = FNil pattern (:>) :: forall n a. n ~ Length (Replicate n a) => forall m. n ~ Succ m => a -> Vec m a -> Vec n a pattern x :> xs <- Identity x :@ xs where x :> xs = Identity x :@ xs
This fails with
/Users/rae/temp/Bug.hs:30:34: error: • Could not deduce: m0 ~ Length xs arising from the "provided" constraints claimed by the signature of ‘:>’ from the context: n ~ Length (Replicate n a) bound by the type signature of pattern synonym ‘:>’ at /Users/rae/temp/Bug.hs:30:11-12 • In the declaration for pattern synonym ‘:>’ • Relevant bindings include xs :: FList Identity xs (bound at /Users/rae/temp/Bug.hs:30:34)
If I comment out the last two lines (the "explicitly bidirectional" part), compilation succeeds, even though the reported error is on the first line of the :>
pattern synonym definition (the pattern part).
Also, the following separate declaration compiles without incident:
(>>>) :: forall n a. n ~ Length (Replicate n a) => forall m. n ~ Succ m => a -> Vec m a -> Vec n a x >>> xs = Identity x :@ xs
I believe the original program should compile, and should continue to compile if I replace the <-
in the patsyn definition with =
.
For the curious: I tried putting an injectivity annotation on Replicate
to avoid those n ~ Length (Replicate n a)
constraints, but type family injectivity just isn't strong enough. Also, I'm not at all sure this definition is any use. But the behavior I report above shouldn't happen, regardless.
Reproducible in HEAD.
Change History (9)
comment:1 Changed 7 months ago by
Cc: | Iceland_jack added |
---|
comment:2 Changed 7 months ago by
comment:3 Changed 7 months ago by
Milestone: | → 8.2.1 |
---|---|
Status: | new → merge |
It seems like this should probably be merged, yes?
comment:7 Changed 7 months ago by
Status: | new → merge |
---|
comment:8 Changed 7 months ago by
comment:2 merged to ghc-8.2
as 8a857f50c5922365c71d07cb403f5c46a75b204e.
comment:9 Changed 7 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
In 7c7479d0/ghc: