Re: [Haskell-cafe] Pattern matching with singletons

2013-03-27 Thread Paul Brauner
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

Re: [Haskell-cafe] Pattern matching with singletons

2013-03-26 Thread Richard Eisenberg
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

[Haskell-cafe] Pattern matching with singletons

2013-03-25 Thread 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