#13735 closed bug (invalid)
RankNTypes don't work with PatternSynonyms
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.0.1 |
Keywords: | PatternSynonyms | Cc: | dfeuer |
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 (last modified by )
data PLambda a = Var a | Int Int | Bool Bool | If (PLambda a) (PLambda a) (PLambda a) | Add (PLambda a) (PLambda a) | Mult (PLambda a) (PLambda a) | Eq (PLambda a) (PLambda a) | Lam (a -> PLambda a) | App (PLambda a) (PLambda a) newtype Lam = L { un :: forall a. PLambda a }
llam :: (forall a. a -> PLambda a) -> Lam llam f = L (Lam f)
works fine, but does not with pattern synonyms:
-- $ ghci -ignore-dot-ghci tirr.hs -- GHCi, version 8.2.0.20170507: http://www.haskell.org/ghc/ :? for help -- [1 of 1] Compiling Main ( tirr.hs, interpreted ) -- -- tirr.hs:20:25: error: -- • Couldn't match expected type ‘forall a. a -> PLambda a’ -- with actual type ‘a0 -> PLambda a0’ -- • In the declaration for pattern synonym ‘LLam’ -- • Relevant bindings include -- a :: a0 -> PLambda a0 (bound at tirr.hs:20:25) -- | -- 20 | pattern LLam a = L (Lam a) -- | ^ -- Failed, modules loaded: none. -- Prelude> pattern LLam :: (forall a. a -> PLambda a) -> Lam pattern LLam a = L (Lam a)
Change History (14)
comment:1 Changed 20 months ago by
comment:2 Changed 20 months ago by
Description: | modified (diff) |
---|
comment:3 Changed 20 months ago by
Re comment:1, it's unsurprising that
llam f = L (Lam f)
with no type signature, does not work. Because f
needs to have a polytype, and it won't without a type sig.
But re the original Description, I agree that the bidirectional definition should go through. I'll take a look.
comment:4 Changed 20 months ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
But re the original Description, I agree that the bidirectional definition should go through
I was wrong. Actually what is happening is quite reasonable.
GHC is rejecting a unidirectional pattern with a signature (bidirectional is red herring):
pattern LLam :: (forall a. a -> PLambda a) -> Lam pattern LLam x <- L (Lam x)
Why rejected? Well, if LLam
had the type claimed by the signature, this would be ok
f1 (LLam x) = (x 'c', x True)
since x :: forall a. a -> PLambda a
. But if you expand the syononym, thus
f2 (L (Lam x)) = (x 'c', x True)
it's clear that f2
should be rejected. (And it is; try it.)
If you doubt that it should be, try to desugar it:
f2 = \(v:Lam). case v of L (w :: forall b. PLambda b) -> case (w @ty) of Lam (x :: ty -> PLambda ty) -> (x 'c', x True)
We pattern match on f2
's argument to extract a polymorphic w
. Then we must apply w
to some type ty
before we can do any more; but now the x
we get from pattern matching is not polymorphic.
Conclusion: it's working fine.
I'll close, but re-open if you disagree
comment:5 Changed 20 months ago by
There is where my intuition breaks down. Writing this works, so higher-rank types + pattern synonyms are fine
newtype A = A (forall xx. xx -> xx) pattern PatA :: (forall xx. xx -> xx) -> A pattern PatA a = A a a :: A -> A a (PatA f) = A f
but I don't understand why this is different
newtype Endo a = Endo (a -> a) newtype B = B (forall xx. Endo xx) pattern PatB :: (a -> a) -> PatB pattern PatB f <- B (Endo f) b :: B -> forall xx. xx -> xx b (B (Endo f)) = f
comment:6 Changed 20 months ago by
It's quite different! As I suggest above, try writing it without the pattern synonym!
comment:7 Changed 20 months ago by
Ah what confused me was that they both (seemingly) allow extracting a polymorphic function
type Id = forall xx. xx -> xx one :: A -> Id one (A f) = f two :: B -> Id two (B (Endo f)) = f
But this doesn't work: (like your f2 (L (Lam x)) = (x 'c', x True)
example demonstrates)
-- works einn :: A -> (Int -> Int, () -> ()) einn (A f) = (f @Int, f @()) -- fails tveir :: B -> (Int -> Int, () -> ()) tveir (B (Endo f)) = (f @Int, f @())
With your desugaring and #11350
A (\@x -> id @x) B (\@x -> Endo @x (id @x))
it becomes clearer to me. Thanks!
comment:8 Changed 20 months ago by
A coworker at work helped me reach this
newtype A = A (forall xx. xx -> xx) newtype Endo a = Endo { appEndo :: a -> a } newtype B = B (forall xx. Endo xx) pattern PatB :: (forall xx. xx -> xx) -> B pattern PatB f <- ((\(B f) -> A (appEndo f)) -> A f) where PatB f = B (Endo f)
which works, the types are in fact isomorphic
to :: A -> B to (A f) = B (Endo f) from :: B -> A from (B f) = A (appEndo f)
similarly with PLambda
data PLambda a = Lam { unLam :: a -> PLambda a } | ... newtype LAM = LAM (forall xx. xx -> PLambda xx) newtype Lam = L (forall a. PLambda a) get :: Lam -> LAM get (L f) = LAM (unLam f) pattern LLAM :: (forall a. a -> PLambda a) -> Lam pattern LLAM f <- (get -> LAM f) where LLAM f = L (Lam f)
comment:9 Changed 20 months ago by
Your get
is partial, so matching on LLAM
will throw an exception (instead of failing) when it doesn't match. It's possible to accomplish your purpose thus:
data Yeah = Yeah (forall a. a -> PLambda a) | Nah getYeah :: Lam -> Yeah getYeah l@(L (Lam _)) = Yeah (case l of L (Lam f) -> f; _ -> error "impossible") getYeah _ = Nah pattern LLam :: (forall a. a -> PLambda a) -> Lam pattern LLam x <- (getYeah -> Yeah x)
It's pretty ugly, though. You have to first pattern match to determine that the constructor is Lam
, then pattern match on the same value again under the Yeah
constructor to capture the polymorphism. If there's a way to avoid that, I don't see it.
comment:10 Changed 20 months ago by
I think what you'd really want would be to have something like
data PLambda' = Var' (forall a. a) | ... | Lam' (forall a. a -> PLambda a) | ...
and then have some non-disgusting way to produce a function
convert :: Lam -> PLambda'
As I said, though, I don't see a nice way.
comment:11 Changed 20 months ago by
Cc: | dfeuer added |
---|
comment:12 follow-up: 13 Changed 20 months ago by
f (B endo) = A (appEndo endo)
works while this doesn't
f :: B -> A f (B (appEndo -> f)) = A f
comment:13 Changed 20 months ago by
Replying to Iceland_jack:
f (B endo) = A (appEndo endo)
works while this doesn'tf :: B -> A f (B (appEndo -> f)) = A f
That's not surprising. We don't have impredicative types, so appEndo x
always produces a monomorphic result. You have to unpack the Endo
under the A
constructor.
Another infelicity of the interaction between
PatternSynonyms
andRankNTypes
is that this unidirectional version typechecks:And this is what GHCi says about the inferred type of
LLam
:But this does not work in an expression context: