Skip to content
Snippets Groups Projects

Type inference failure in bidirectional pattern synonym and GADT pattern match

    • Closed Issue created by Richard Eisenberg @rae

    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
    To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

    Child items ...

    • Activity

    Please register or sign in to reply