Skip to content

Nested RankNType fails to compile

GHC 8.10.2: Here are pretty sensible pattern synonyms for E a b: a Church encoding of Either a b.

{-# Language PatternSynonyms          #-}
{-# Language ImpredicativeTypes       #-}
{-# Language RankNTypes               #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language ViewPatterns             #-}

import Data.Kind

type E :: Type -> Type -> Type
type E a b = forall res. (a -> res) -> (b -> res) -> res

pattern ELeft :: a -> E a b
pattern ELeft a <- ((\e -> e Just (const Nothing)) -> Just a)
  where ELeft a left _right = left a

pattern ERight :: b -> E a b
pattern ERight b <- ((\e -> e (const Nothing) Just) -> Just b)
  where ERight b _left right = right b

When using them in nested positions, inference fails. Maybe this has been fixed or is not supposed to type check, but each of the 3 clauses of regroup fail to compile.

regroup :: forall a b c. E a (E b c) -> E (E a b) c

-- • Couldn't match type ‘(a -> res0) -> (b0 -> res0) -> res0’
--                  with ‘forall res1. (a -> res1) -> (b -> res1) -> res1’
--   Expected type: (E a b -> res) -> (c -> res) -> res
--     Actual type: (((a -> res0) -> (b0 -> res0) -> res0) -> res)
--                  -> (c -> res) -> res
regroup (ELeft a) = ELeft (ELeft a)

-- • Couldn't match expected type ‘E b0 b1’
--               with actual type ‘(b -> res1) -> (c -> res1) -> res1’

-- • Couldn't match type ‘(a0 -> res0) -> (b0 -> res0) -> res0’
--                  with ‘forall res2. (a -> res2) -> (b -> res2) -> res2’
--   Expected type: (E a b -> res) -> (c -> res) -> res
--     Actual type: (((a0 -> res0) -> (b0 -> res0) -> res0) -> res)
--                  -> (c -> res) -> res
regroup (ERight (ELeft b)) = ELeft (ERight b)

-- • Couldn't match expected type ‘E a0 c’
--               with actual type ‘(b -> res0) -> (c -> res0) -> res0’
regroup (ERight (ERight c)) = ERight c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information