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 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.

Change History (1)

comment:1 Changed 9 days ago by Iceland_jack

Cc: Iceland_jack added
Note: See TracTickets for help on using tickets.