1 Jun 2012 10:37
#6137: Different behaviour between a GADT and a data family with regards to kind unification
GHC <cvs-ghc <at> haskell.org>
2012-06-01 08:37:03 GMT
2012-06-01 08:37:03 GMT
#6137: Different behaviour between a GADT and a data family with regards to kind
unification
------------------------------+---------------------------------------------
Reporter: dreixel | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 7.5 | Keywords: PolyKinds
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby: | Blocking:
Related: |
------------------------------+---------------------------------------------
We have discussed this before, but I don't remember if this was classified
as a bug or as a "known feature" of GADTs. Given the following code:
{{{
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
data Sum a b = L a | R b
data Sum1 (a :: k1 -> *) (b :: k2 -> *) :: Sum k1 k2 -> * where
LL :: a i -> Sum1 a b (L i)
RR :: b i -> Sum1 a b (R i)
data Code i o = F (Code (Sum i o) o)
}}}
(Continue reading)
RSS Feed