Opened 11 months ago
Closed 10 months ago
#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 11 months ago by
Cc: | mpickering cactus added |
---|
comment:2 Changed 11 months ago by
Keywords: | PatternSynonyms added |
---|
comment:3 Changed 11 months ago by
Ewww. In the representation of PatSyn
s, 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 11 months ago by
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 11 months ago by
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 10 months ago by
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) = ...
comment:7 Changed 10 months ago by
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
comment:8 Changed 10 months ago by
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 10 months ago by
No quantification needed if returning a type synonym:
type Arr = (->) pattern App :: b -> Arr Char b pattern App b <- (($ 'a') -> b)
comment:12 Changed 10 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → patsyn/should_compile/T11977 |
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
(wherea
,b
, andc
are arbitrary types, not necessarily variables; that is, they are metavariables), we've been saying thata
andb
are arguments to the pattern andc
is the result type. But in your case, the type isa -> Char -> a
, andChar -> a
is the result type. Yet there is no way to indicate this in a type signature. I even trieda -> (Char -> a)
to no avail.I have no suggestions (other than parentheses, which would be awkward) for how to fix this.