Idris-dev/test/error003/expected

ErrorReflection.idr:67:5:When elaborating right hand side of bad:
DSL type error: (t(502) => t'(503)) doesn't match ()
Remove the ability to reflect At and Elaborating This is because they are primarily "plumbing" for tracking error locations, so it's better for error reflection to work on their payloads. Any reasonable implementation would have just copied what the compiler does with them anyway. 2014-03-10 17:40:17 +04:00			`ErrorReflection.idr:67:5:When elaborating right hand side of bad:`
Better treatment of unbound implicits Now uses the elaborator to generate any necessary extra bindings, using the same machinery as pattern match elaboration. The end result is that you no longer need 'using' in a lot of cases (it is still useful if you want to give explicit types, of course). e.g. this now works as it stands: data Elem : a -> Vect n a -> Type where Here : Elem x (x :: xs) There : Elem x xs -> Elem x (y :: xs) isElem : DecEq a => (x : a) -> (xs : _) -> Maybe (Elem x xs) This should also reduce the number of weird "no such variable" errors signfificantly. In particular, it fixes #1354 2014-07-08 05:40:37 +04:00			`DSL type error: (t(502) => t'(503)) doesn't match ()`