Paul Brauner | 25 Mar 19:02 2013

Pattern matching with singletons


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?
Haskell-Cafe mailing list
Haskell-Cafe <at>