| 139 | = Type Inference = |

| 140 | |

| 141 | Figuring out type inference for this language is a bit of a challenge. While the full design won't be laid out here, interesting tidbits will be gathered here for easy retrieval. |

| 142 | |

| 143 | === Inferring `pi` types === |

| 144 | |

| 145 | Suppose a programmer writes, without a type signature |

| 146 | |

| 147 | {{{ |

| 148 | foo @Zero y = y |

| 149 | }}} |

| 150 | |

| 151 | (Here, we are assuming `@` as the invisible-overrider.) What is `foo`'s type? It could be `pi (n :: Nat). forall (a :: *). Vec a n -> Vec a Zero`. It could also be `forall (n :: Nat) (a :: *). a -> a`. Neither is more general than the other -- we are in the same GADT type-inference problem as described in the [http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf OutsideIn] paper. Thus, we reject such a `foo` that matches on an implicit parameter without a type signature. |

| 152 | |

| 153 | But, what about |

| 154 | {{{ |

| 155 | foo Zero y = y |

| 156 | }}} |

| 157 | |

| 158 | We are actually in the same situation here. But, backward compatibility compels us to prefer non-dependent types over dependent ones, inferring `foo :: forall (a :: *). Nat -> a -> a`. (Note that `foo :: forall (a :: *). pi (n :: Nat) -> Vec a n -> Vec a Zero` is a valid but incomparable type that we could assign.) |

| 159 | |

| 160 | When do `pi`-types get inferred, if ever? Good question. |

| 161 | |

| 162 | = Implementation = |

| 163 | |

| 164 | The implementation of this is under way, [https://github.com/goldfirere/ghc/tree/nokinds here]. More notes will be added to this section in due course. |

| 165 | |