Paul Brauner | 25 Mar 19:02 2013
Picon
Gravatar

Pattern matching with singletons

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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane