Opened 9 days ago

Last modified 9 days ago

## #13441 new bug

# Type inference failure in bidirectional pattern synonym and GADT pattern match

Reported by: | goldfire | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

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.

**Note:**See TracTickets for help on using tickets.