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