Very helpful, thanks! I may come back with more singleton/type families
questions :)
On Tue, Mar 26, 2013 at 6:41 PM, Richard Eisenberg e...@cis.upenn.eduwrote:
Hello Paul,
- Forwarded message from Paul Brauner polux2...@gmail.com -
snip
- is a ~ ('CC ('Left 'CA)) a
Hello Paul,
- Forwarded message from Paul Brauner polux2...@gmail.com -
snip
- 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
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