#11977 closed bug (fixed)

ghc doesn't agree with its own inferred pattern type

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.1
Keywords: PatternSynonyms Cc: mpickering, cactus
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: patsyn/should_compile/T11977
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

GHCi, version 8.1.20160419:

pattern F a <- (($ 'a') -> a)
>>> :i F
pattern F :: b -> Char -> b 	-- Defined at /tmp/tTaa.hs:24:1

Putting them together:

-- tTaa.hs:25:9: error: …
--     • Pattern synonym ‘F’ has one argument
--         but its type signature has two
--     • In the declaration for pattern synonym ‘F’
Compilation failed.
pattern F :: b -> Char -> b 
pattern F a <- (($ 'a') -> a)

Change History (12)

comment:1 Changed 20 months ago by goldfire

Cc: mpickering cactus added

Very interesting test case!

You've discovered that, once again, we've misunderstood pattern types.

If you assign a pattern the type a -> b -> c (where a, b, and c are arbitrary types, not necessarily variables; that is, they are metavariables), we've been saying that a and b are arguments to the pattern and c is the result type. But in your case, the type is a -> Char -> a, and Char -> a is the result type. Yet there is no way to indicate this in a type signature. I even tried a -> (Char -> a) to no avail.

I have no suggestions (other than parentheses, which would be awkward) for how to fix this.

comment:2 Changed 20 months ago by cactus

Keywords: PatternSynonyms added

comment:3 Changed 20 months ago by cactus

Ewww. In the representation of PatSyns, the types of arguments and the type of the scrutinee are stored separately, so that shouldn't be an issue. However, I have no idea what the surface syntax should be for presenting such a type.

comment:4 Changed 20 months ago by simonpj

I had always taken it for granted that a pattern synonym described a data type, not a function. It's hard to pattern match in an interesting way on a function, short of calling it I suppose.

Lacking compelling examples, I'm inclined to add the requirement that the result type of a pattern synonym is a data type.

Simon

comment:5 Changed 20 months ago by goldfire

But it currently can be a type variable (when constrained by a class). If we don't allow functions to be matched against in this way, we lose substitution. This isn't a killer (it's all surface Haskell and in no way is a type safety issue), just a bit suboptimal to me.

I actually think the original example looks potentially useful. I could see waiting until someone presents an actual use case they wish to use in real code, though.

comment:6 Changed 19 months ago by Iceland_jack

Here's is an odd thing, it works if you quantify it!

--   Doesn't work!
-- pattern F :: b -> Char -> b
-- pattern F a <- (($ 'a') -> a)

--   Does work for some reason
pattern F1 :: b -> forall x. Char -> b
pattern F1 a <- (($ 'a') -> a)

--   Wait what?
pattern F2 :: b -> forall b. Char -> b
pattern F2 a <- (($ 'a') -> a)

How does this play out

--   Inferred type
f1 :: (forall (x :: k). Char -> b) -> b
f1 (F1 x) = x

--   Works exactly like:
-- 
--     f1 (($ 'a') -> x) = x
-- 
f1 :: (Char -> b) -> b
f1 (F1 x) = x

with F2:

f2 :: (forall b. Char -> b) -> b1
f2 (F2 x) = ...
Last edited 19 months ago by Iceland_jack (previous) (diff)

comment:7 Changed 19 months ago by Iceland_jack

Noticed while looking at Carter's copatterns and saw that the following compiles:

type Stream a = forall res . StreamTag a res -> res

data StreamTag a res where 
   HeadTag :: StreamTag a a 
   -- TailTag :: StreamTag a (Stream a)

pattern Head' :: res -> Stream res
pattern Head' x <- (($ HeadTag) -> x)

but it is my understanding that Stream must be a newtype/data (generative) to be able to define TailTag:

newtype Stream a = Stream (forall res. StreamTag a res -> res)

data StreamTag a res where 
   HeadTag :: StreamTag a a 
   TailTag :: StreamTag a (Stream a)

pattern Head :: a -> Stream a
pattern Head x <- ((\(Stream str) -> str HeadTag) -> x)

pattern Tail :: Stream a -> Stream a
pattern Tail xs <- ((\(Stream str) -> str TailTag) -> xs)

pattern Cons :: a -> Stream a -> Stream a
pattern Cons x xs <- ((\(Stream str) -> (str HeadTag, str TailTag)) -> (x, xs))

headStream :: Stream a -> a 
headStream (Head x) = x

tailStream :: Stream a -> Stream a 
tailStream (Tail xs) = xs

rawRawZipWith :: (a -> b -> c) -> (Stream a -> Stream b -> Stream c)
rawRawZipWith f sta stb = Stream $ \str -> do
  let Head x  = sta
      Head y  = stb
      Tail xs = sta
      Tail ys = stb
  
  case str of 
    HeadTag -> f x y
    TailTag -> rawRawZipWith f xs ys

rawRawZipWith' :: (a -> b -> c) -> (Stream a -> Stream b -> Stream c)
rawRawZipWith' f (Cons x xs) (Cons y ys) = Stream $ \case
  HeadTag -> f x y
  TailTag -> rawRawZipWith f xs ys

Last edited 19 months ago by Iceland_jack (previous) (diff)

comment:8 Changed 19 months ago by Iceland_jack

Just fooling around

pattern Mempty :: Monoid a => b -> forall x. a -> b
pattern Mempty b <- (($ mempty) -> b)
  where Mempty b _ = b
pattern Mempty :: b -> forall a. (Eq a, Monoid a) => a -> b
pattern Mempty b <- (($ mempty @String) -> b)
  where Mempty b _ = b

foo :: (forall a. (Eq a, Monoid a) => a -> b) -> b
foo (Mempty x) = x
ghci> foo (== mempty)
True
ghci> :t Mempty 'a'
Mempty 'a' :: forall {a}. (Monoid a, Eq a) => a -> Char
ghci> :t foo (Mempty 'a')
foo (Mempty 'a') :: Char
ghci> foo (Mempty 'a')
'a'

or

type MEMPTY b = forall a. (Eq a, Monoid a) => a -> b

pattern Mempty :: b -> MEMPTY b

comment:9 Changed 19 months ago by Iceland_jack

No quantification needed if returning a type synonym:

type Arr = (->)

pattern App :: b -> Arr Char b
pattern App b <- (($ 'a') -> b)

comment:10 Changed 19 months ago by simonpj

I have a fix in the works

comment:11 Changed 19 months ago by Simon Peyton Jones <simonpj@…>

In 03d89603/ghc:

Don't split the arg types in a PatSyn signature

This patch fixes Trac #11977, and #12108, rather satisfactorily
maily by deleting code!

  pattern P :: Eq a => a -> a -> Int

The idea is simply /not/ to split the bit after the '=>' into the
pattern argument types, but to keep the (a->a->Int) part
un-decomposed, in the patsig_body_ty field of a TcPatSynInfo.

There is one awkward wrinkle, which is that we can't split the
implicitly-bound type variables into existential and universal until
we know which types are arguments and which are part of the result.
So we postpone the decision until we have the declaration in hand.
See TcPatSyn Note [The pattern-synonym signature splitting rule]

comment:12 Changed 19 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: patsyn/should_compile/T11977
Note: See TracTickets for help on using tickets.