Opened 5 months ago

Closed 5 months ago

Last modified 5 months ago

#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 Iceland_jack)

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 5 months ago by RyanGlScott

Another infelicity of the interaction between PatternSynonyms and RankNTypes is that this unidirectional version typechecks:

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where

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 }

pattern LLam a <- L (Lam a)

And this is what GHCi says about the inferred type of LLam:

GHCi, version 8.3.20170516: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, modules loaded: Bug.
λ> :i LLam
pattern LLam :: (a -> PLambda a) -> Lam         -- Defined at Bug.hs:13:1

But this does not work in an expression context:

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Bug where

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 f = L (Lam f)
GHCi, version 8.3.20170516: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:13:17: error:
    • Couldn't match expected type ‘a -> PLambda a’
                  with actual type ‘p’
        because type variable ‘a’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          forall a. PLambda a
        at Bug.hs:13:10-18
    • In the first argument of ‘Lam’, namely ‘f’
      In the first argument of ‘L’, namely ‘(Lam f)’
      In the expression: L (Lam f)
    • Relevant bindings include
        f :: p (bound at Bug.hs:13:6)
        llam :: p -> Lam (bound at Bug.hs:13:1)
   |
13 | llam f = L (Lam f)
   |                 ^

comment:2 Changed 5 months ago by Iceland_jack

Description: modified (diff)

comment:3 Changed 5 months ago by simonpj

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 5 months ago by simonpj

Resolution: invalid
Status: newclosed

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 5 months ago by Iceland_jack

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 5 months ago by simonpj

It's quite different! As I suggest above, try writing it without the pattern synonym!

comment:7 Changed 5 months ago by Iceland_jack

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!

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

comment:8 Changed 5 months ago by Iceland_jack

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)
Last edited 5 months ago by Iceland_jack (previous) (diff)

comment:9 Changed 5 months ago by dfeuer

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 5 months ago by dfeuer

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 5 months ago by dfeuer

Cc: dfeuer added

comment:12 Changed 5 months ago by Iceland_jack

f (B endo) = A (appEndo endo) works while this doesn't

f :: B -> A
f (B (appEndo -> f)) = A f

comment:13 in reply to:  12 Changed 5 months ago by dfeuer

Replying to Iceland_jack:

f (B endo) = A (appEndo endo) works while this doesn't

f :: 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.

comment:14 Changed 5 months ago by Iceland_jack

Very cool

Note: See TracTickets for help on using tickets.