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