[Haskell-cafe] Pattern matching with singletons

[Paul Brauner]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130325/4d867233/attachment.htm>