Type family fails to reduce when unmatchable application is involved
The title of this issue is rather vague, but I'm not quite sure how to describe this phenomenon. I originally noticed this when attempting to port over the singletons
test suite, as there was a specific piece of code that worked with a defunctionalized unmatchable arrow, but not with (->) @U
. Here is a minimized version of that code:
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ >= 811
{-# LANGUAGE UnsaturatedTypeFamilies #-}
#endif
module Bug where
import Data.Kind
#if __GLASGOW_HASKELL__ >= 811
import GHC.Exts
#endif
type Hm :: (a ~> Bool) -> a -> Bool
type family Hm f x where
Hm f x = HmCase (f @@ x)
type HmCase :: Bool -> Bool
type family HmCase b where
HmCase True = False
HmCase False = True
sHm :: forall a (f :: a ~> Bool) (x :: a).
Sing f -> Sing x -> Sing (Hm f x)
sHm sF sX = case sF @@ sX of
STrue -> SFalse
SFalse -> STrue
-----
type Sing :: k -> Type
type family Sing :: k -> Type
type SBool :: Bool -> Type
data SBool z where
SFalse :: SBool False
STrue :: SBool True
type instance Sing = SBool
type SLambda :: forall k1 k2. (k1 ~> k2) -> Type
newtype SLambda (f :: k1 ~> k2) =
SLambda { (@@) :: forall t. Sing t -> Sing (f @@ t) }
type instance Sing = SLambda
#if __GLASGOW_HASKELL__ >= 811
type (~>) :: Type -> Type -> Type
type a ~> b = a -> @U b
type (@@) :: (k1 ~> k2) -> k1 -> k2
type family f @@ x where
f @@ x = f x
#else
type TyFun :: Type -> Type -> Type
data TyFun x y
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
type (@@) :: (k1 ~> k2) -> k1 -> k2
type family f @@ x
#endif
The CPP in this program is only included to allow this file to be compile with both GHC 8.10 (which uses defunctionalization) and your fork (which uses (->) @U
). This compiles with GHC 8.10, but not with your fork:
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:34:13: error:
• Could not deduce: HmCase (f x) ~ 'False
from the context: f x ~ 'True
bound by a pattern with constructor: STrue :: SBool 'True,
in a case alternative
at Bug.hs:34:3-7
Expected: Sing (Hm f x)
Actual: SBool 'False
• In the expression: SFalse
In a case alternative: STrue -> SFalse
In the expression:
case sF @@ sX of
STrue -> SFalse
SFalse -> STrue
• Relevant bindings include
sX :: Sing x (bound at Bug.hs:33:8)
sF :: Sing f (bound at Bug.hs:33:5)
sHm :: Sing f -> Sing x -> Sing (Hm f x) (bound at Bug.hs:33:1)
|
34 | STrue -> SFalse
| ^^^^^^
Bug.hs:35:13: error:
• Could not deduce: HmCase (f x) ~ 'True
from the context: f x ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in a case alternative
at Bug.hs:35:3-8
Expected: Sing (Hm f x)
Actual: SBool 'True
• In the expression: STrue
In a case alternative: SFalse -> STrue
In the expression:
case sF @@ sX of
STrue -> SFalse
SFalse -> STrue
• Relevant bindings include
sX :: Sing x (bound at Bug.hs:33:8)
sF :: Sing f (bound at Bug.hs:33:5)
sHm :: Sing f -> Sing x -> Sing (Hm f x) (bound at Bug.hs:33:1)
|
35 | SFalse -> STrue
| ^^^^^
This seems like it ought to typecheck. Since HmCase True = False
, shouldn't GHC be able to deduce HmCase (f x) ~ 'False
from f x ~ 'True
?