#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 8 months ago by
comment:2 Changed 8 months ago by
Description: | modified (diff) |
---|
comment:3 Changed 8 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 8 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 8 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 8 months ago by
It's quite different! As I suggest above, try writing it without the pattern synonym!
comment:7 Changed 8 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 8 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 8 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 8 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 8 months ago by
Cc: | dfeuer added |
---|
comment:12 follow-up: 13 Changed 8 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 8 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: