Opened 6 weeks ago

Closed 4 weeks ago

#13441 closed bug (fixed)

Type inference failure in bidirectional pattern synonym and GADT pattern match

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.2.1
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 (9)

comment:1 Changed 6 weeks ago by Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 5 weeks ago by Simon Peyton Jones <simonpj@…>

In 7c7479d0/ghc:

Fix explicitly-bidirectional pattern synonyms

This partly fixes Trac #13441, at least for the explicitly
bidirectional case.

See Note [Checking against a pattern signature], the part about
"Existential type variables".

Alas, the implicitly-bidirectional case is still not quite right, but
at least there is a workaround by making it explicitly bidirectional.

comment:3 Changed 5 weeks ago by bgamari

Milestone: 8.2.1
Status: newmerge

It seems like this should probably be merged, yes?

comment:4 Changed 5 weeks ago by simonpj

Yes.

comment:5 Changed 5 weeks ago by Simon Peyton Jones <simonpj@…>

In b5c81203/ghc:

Complete the fix for #13441 (pattern synonyms)

Do not attempt to typecheck both directions of an
implicitly-bidirectional pattern synonym simultanously,
as we were before.  Instead, the builder is typechecked
when we typecheck the code for the builder, which was
of course happening already, even in both bidirectional
cases.

See Note [Checking against a pattern signature], under
"Existential type variables".

comment:6 Changed 5 weeks ago by simonpj

Status: mergenew

Probably worth merging this too.

comment:7 Changed 5 weeks ago by simonpj

Status: newmerge

comment:8 Changed 4 weeks ago by bgamari

comment:9 Changed 4 weeks ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.