Very helpful, thanks! I may come back with more singleton/type families
questions :)
On Tue, Mar 26, 2013 at 6:41 PM, Richard Eisenberg wrote:
> Hello Paul,
>
> > - Forwarded message from Paul Brauner -
>
>
>
> > - is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC,
> >
Hello Paul,
> - Forwarded message from Paul Brauner -
> - 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 (
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
