[GHC] #13441: Type inference failure in bidirectional pattern synonym and GADT pattern match

[GHC]

#13441: Type inference failure in bidirectional pattern synonym and GADT pattern
match
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternSynonyms                    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13441>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler