In this code
data ValueA :: forall (k :: *1). (k ~> *0) ~> k ~> *0 where
A :: forall (k :: *1) m (n :: k). m n -> ValueA m n
data ValueB :: forall (k :: *1). (k ~> *0) ~> k ~> *0 where
B :: forall (k :: *1) (m :: k ~> *0) (n :: k). m n -> ValueB m n
ValueA and ValueB should work the same. They mostly do - both can be used as
constructors and in pattern matching. But ":t A" gives an error, and ":t B"
works well.
prompt> :t A
Different types
'b != 'a
(dbd,ebd)
prompt> :t B
B :: forall (a:*1) (b:a ~> *0) (c:a:*1).b c -> ValueB b c
Original issue reported on code.google.com by krz.gogo...@gmail.com on 30 Aug 2011 at 12:50
Original issue reported on code.google.com by
krz.gogo...@gmail.com
on 30 Aug 2011 at 12:50