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 FLists (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