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