david-christiansen
commented
9 years ago This is really a problem with dependent function composition in general - it needs to cleverly invent types to give as arguments to (.), or rely on the user to specify them. So when you start getting into more dependent compositions, things will start to fail like this, and there's nothing we can do about it without investing a few PhDs into type inference for (.). A point-free style has different trade-offs in a dependently typed language than it does in a H-M language.
Our error message should be better here, though!
The dsl syntax extension in (https://github.com/ISANobody/SILL-Idris/blob/master/Sessions.idr line 244) fails with "No such variable k" when variable is defined as
Var . Justbut it works when replaced with a toplevel binding that does\i => Var (Just i). Given that there is no explicitkanywhere (but multiple implicit ones), this is pretty confusing.