On Sat, Apr 4, 2015 at 5:52 AM, Keean Schupke <[email protected]> wrote: > On 4 April 2015 at 10:38, Matt Oliveri <[email protected]> wrote: ... >> > Type inference is fine :-) Note the Types are a kind of >> > type-level-object, >> > so the can be an inferable subset of all type-level-objects. >> >> Good point. But if we allow the user to write a type outside the >> subset, it could mess things up, right? So to preserve type inference >> you'd need to rule it out in some way. > > If Types are an inferable subset of type-level-objects, you could write any > type and it should not mess up type-inference. If you wrote a > type-level-expression that was not a Type, it would not be a valid type! It > would be a type level expression. > > With type-level logic programming, we would say the type-level program needs > to evaluate to true in order for the program to compile, else it would > return an error. Much like a type-level assertion. Such expressions could > be made of Type kinds and non-Type kinds, but types must be Types.
You are missing the point. Type-level expressions may not denote types, but the point of type-level expressions is they will be used as subexpressions for type expressions. In order to ensure that type inference algorithms do not encounter cases they can't handle, we generally need to restrict types on the basis of the non-type subexpressions they can use. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
