@edwinbrady does idris use any especially interesting technique to elaborate implicit things like foralls and constraints?
Not really - for implicits it generates a metavariable, which will hopefully be solved in the course of solving unification problems. Auto implicits (constraints) are solved by a type driven search. I think it's fairly standard, in so far as there is a "standard" here at all.
-
-
how does idris handle cases like M : forall a. B -> C a ~ B -> forall a. C a?? does it do re-abstraction as necessary or??
-
Is this about the second 'a'? That'd be a new variable, just as if it had a different name. Or do you mean something else? (embarrassingly I can't remember what the ~ means just now...)
- 3 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.