Opened 3 years ago
Closed 3 years 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 3 years ago by
Cc: | mpickering cactus added |
---|
comment:2 Changed 3 years ago by
Keywords: | PatternSynonyms added |
---|
comment:3 Changed 3 years 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 3 years 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 3 years 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 3 years 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 3 years 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 3 years 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 3 years 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 3 years 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.