I don't think we'll need notation to differentiate: just use overloaded literals, like we do in terms. Something that would operate vaguely like this:
type family 3 :: k where
3 :: Nat = ... -- 3 as a Nat
3 :: Integer = ... -- 3 as an Integer
I'm not at all suggesting it be implemented this way, but we already have the ability to branch in type families based on result kind, so the mechanism is already around. Unfortunately, this would be unhelpful if the user asked for (3 :: Bool), which would kind-check but be stuck.
Richard
Hello,
actually type-level integers are easier to work with than type-level naturals (e.g., one can cancel things by subtracting at will). I agree that ideally we want to have both integers and naturals (probably as separate kinds). I just don't know what notation to use to distinguish the two.
-Iavor