I really don't like the way scoping works in Idris. I feel like it tries to do too much automagically & just fails to understand what I mean
-
-
Replying to @anormalform
Case in point: I have `lt : a -> a -> Type` as a data parameter but in constructors it's resolved as the function `lt : a -> a -> Bool`...
1 reply 0 retweets 0 likes -
Replying to @anormalform
Then I get an obscure error message telling me there's a type mismatch. No there's not. A parameter should shadow whatever Prelude brings in
1 reply 0 retweets 0 likes -
Replying to @anormalform
While I'm at it: I'd like to use vars starting with a Capital without it guessing it's a Cons. I want to write `(a : A)`, not `(eltA : a)`.
1 reply 0 retweets 1 like -
-
Replying to @anormalform
@eisaru There are rules for this… it isn't trying to read your mind.
2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@eisaru Even so, can you show me your code? Error messages should explain this problem, and ought to have got better recently.
2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady It's all fixed (I was working on the FreshList I sent to the ML). I have '0.9.19.1' so the error msgs may have gotten better ;)1 reply 0 retweets 0 likes
@eisaru oh. An ancient version, we're on 0.11 now. There could easily have been an error in the scoping rules implementation then.
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.