| 89 | |

| 90 | |

| 91 | == Interaction with normal functions == |

| 92 | |

| 93 | Functions cannot have arguments of a non * kind. So the following would be disallowed: |

| 94 | |

| 95 | {{{ |

| 96 | bad :: Zero -> Bool -- Zero has kind Nat |

| 97 | }}} |

| 98 | |

| 99 | This follows straighforwardly from the kind of (->) in GHC already: {{{?? -> ? -> *}}}, see IntermediateTypes |

| 100 | |

| 101 | Type variables may however be inferred to have non-* kinds. E.g. |

| 102 | |

| 103 | {{{ |

| 104 | #!text/x-haskell |

| 105 | data NatRep :: Nat -> * where |

| 106 | ZeroRep :: NatRep Zero |

| 107 | SuccRep :: (NatRep n) -> NatRep (Succ n) |

| 108 | |

| 109 | tReplicate :: forall n a . NatRep n -> a -> List a n |

| 110 | ... |

| 111 | }}} |

| 112 | |

| 113 | In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind {{{*}}}. |

| 114 | |

107 | | ~~== Interaction with normal functions ==~~ |

108 | | |

109 | | ~~Functions cannot have arguments of a non * kind. So the following would be disallowed:~~ |

110 | | |

111 | | ~~{{{~~ |

112 | | ~~bad :: Zero -> Bool -- Zero has kind Nat~~ |

113 | | ~~}}}~~ |

114 | | |

115 | | ~~This follows straighforwardly from the kind of (->) in GHC already: {{{?? -> ? -> *}}}, see IntermediateTypes~~ |

116 | | |

117 | | ~~Type variables may however be inferred to have non-* kinds. E.g.~~ |

118 | | |

119 | | ~~{{{~~ |

120 | | ~~#!text/x-haskell~~ |

121 | | ~~data NatRep :: Nat -> * where~~ |

122 | | ~~ ZeroRep :: NatRep Zero~~ |

123 | | ~~ SuccRep :: (NatRep n) -> NatRep (Succ n)~~ |

124 | | |

125 | | ~~tReplicate :: forall n a . NatRep n -> a -> List a n~~ |

126 | | ~~...~~ |

127 | | ~~}}}~~ |

128 | | |

129 | | ~~In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind {{{*}}}.~~ |

130 | | |