Some type-family rules are ignored when deducing equality constraints under GADT match
With GHC 8.8.3:
Test.hs
{-# LANGUAGE GADTs, TypeFamilies, PolyKinds, DataKinds, ConstraintKinds, TypeOperators, PolyKinds,
RankNTypes, ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
UndecidableInstances, LambdaCase, EmptyCase, TypeFamilyDependencies #-}
import Data.Kind
import GHC.TypeLits
import Data.Singletons
import Data.Singletons.TypeLits
import Data.Singletons.Decide
data TMaybe (t :: Maybe k) where
TNothing :: TMaybe 'Nothing
TJust :: !t -> TMaybe ('Just t)
data KVList (kk :: [Symbol]) (vv :: [Type]) :: Type where
KVNil :: KVList '[] '[]
KVCons :: !(Sing k) -> !v -> !(KVList kk vv) -> KVList (k : kk) (v : vv)
type family LookupKV (k :: Symbol) (tab :: Type) = v where
LookupKV k (KVList '[] '[]) = TMaybe 'Nothing
LookupKV k (KVList (k ': kk1) (v ': vv1)) = TMaybe ('Just v)
LookupKV k (KVList (k1 ': kk1) (v ': vv1)) = LookupKV k (KVList kk1 vv1)
lookupKV
:: Sing k -> KVList kk vv -> LookupKV k (KVList kk vv)
lookupKV k = \case
KVNil -> TNothing
KVCons k' v r -> case k %~ k' of
Proved Refl -> TJust v
Disproved d -> lookupKV k r
The last line gives:
• Could not deduce: LookupKV k (KVList kk1 vv1)
~ LookupKV k (KVList (k1 : kk1) (v : vv1))
from the context: (kk ~ (k1 : kk1), vv ~ (v : vv1))
bound by a pattern with constructor:
KVCons :: forall (k :: Symbol) v (kk :: [Symbol]) (vv :: [*]).
Sing k -> v -> KVList kk vv -> KVList (k : kk) (v : vv),
in a case alternative
at Test.hs:28:3-15
Expected type: Decision (LookupKV k (KVList kk vv))
Actual type: Decision (LookupKV k (KVList kk1 vv1))
With -fprint-explicit-kinds
:
• Could not deduce: (LookupKV k (KVList kk1 vv1) :: *)
~ (LookupKV k (KVList ((':) @Symbol k1 kk1) ((':) @* v vv1)) :: *)
from the context: ((kk :: [Symbol])
~ ((':) @Symbol k1 kk1 :: [Symbol]),
(vv :: [*]) ~ ((':) @* v vv1 :: [*]))
bound by a pattern with constructor:
KVCons :: forall (k :: Symbol) v (kk :: [Symbol]) (vv :: [*]).
Sing @Symbol k
-> v -> KVList kk vv -> KVList ((':) @Symbol k kk) ((':) @* v vv),
in a case alternative
at Test.hs:28:3-15
which doesn't seem to raise anything suspicious, all the kinds are fully-resolved and contain no variables that could be ambiguous.
But in the definition for type family LookupKV
it specifically says
LookupKV k (KVList (_ ': kk) (v ': vv)) = LookupKV k (KVList kk vv)
Considering the fact the Proved (TJust v)
branch type-checks, GHC must have deduced LookupKV k (KVList (k ': kk1) (v ': vv1)) ~ TMaybe ('Just v)
via the corresponding type-family rule. So it's strange it doesn't use another type-family rule for this unsatisfied deduction. I'm pretty sure this is unrelated to injectivity since k, kk, and vv all appear as themselves in the actual type signature, unapplied to a type family.