Hello, the following programs seems to hit either some limitation of GHC or maybe I'm just missing something and it behaves the intended way. {-# LANGUAGE TemplateHaskell, TypeFamilies, DataKinds, GADTs #-} module Test where import Data.Singletons data TA = CA data TB = CB data TC = CC (Either TA TB) $(genSingletons [''TA, ''TB, ''TC]) type family Output (x :: TC) :: * type instance Output ('CC ('Left 'CA)) = Int type instance Output ('CC ('Right 'CB)) = String f :: Sing (a :: TC) -> Output a f (SCC (SLeft SCA)) = 1 g :: Sing (a :: TC) -> Output a g (SCC (SLeft _)) = 1 Function f typechecks as expected. Function g fails to typecheck with the following error. Could not deduce (Num (Output ('CC ('Left TA TB n0)))) arising from the literal `1' from the context (a ~ 'CC n, SingRep (Either TA TB) n) bound by a pattern with constructor SCC :: forall (a_a37R :: TC) (n_a37S :: Either TA TB). (a_a37R ~ 'CC n_a37S, SingRep (Either TA TB) n_a37S) => Sing (Either TA TB) n_a37S -> Sing TC a_a37R, in an equation for `g' at Test.hs:21:4-16 or from (n ~ 'Left TA TB n0, SingRep TA n0, SingKind TA ('KindParam TA)) bound by a pattern with constructor SLeft :: forall (a0 :: BOX) (b0 :: BOX) (a1 :: Either a0 b0) (n0 :: a0). (a1 ~ 'Left a0 b0 n0, SingRep a0 n0, SingKind a0 ('KindParam a0)) => Sing a0 n0 -> Sing (Either a0 b0) a1, in an equation for `g' at Test.hs:21:9-15 Possible fix: add an instance declaration for (Num (Output ('CC ('Left TA TB n0)))) In the expression: 1 In an equation for `g': g (SCC (SLeft _)) = 1 I would expect that a ~ ('CC ('Left 'CA)) in the right hand-side of g (SCC (SLeft _)) = 1 since SLeft's argument is necessarily of type STA, whose sole inhabitant is SA. Now I understand (looking at -ddump-slices, the singletons' library paper and the error message) that the definition of SCC and SLeft don't immediately imply what I just wrote above. So my question is: in the right hand-side of g (SCC (SLeft _)) = 1, - is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC, SLeft, ... (in which case GHC could infer it but for some reason can't) - or are these pattern + definitions not sufficient to prove that a ~ ('CC ('Left 'CA)) no matter what? Cheers, Paul