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

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.

## Trac metadata

Trac field | Value |
---|---|

Version | 8.1 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |