idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.42k stars 643 forks source link

:let fails on infix specifications #1420

Closed david-christiansen closed 9 years ago

david-christiansen commented 10 years ago
Idris> :let infixr 7 <==|
src/Idris/REPL.hs:(681,3)-(692,50): Non-exhaustive patterns in function defineName

Idris> :let infixr 7 @@@
src/Idris/REPL.hs:(681,3)-(692,50): Non-exhaustive patterns in function defineName
david-christiansen commented 10 years ago

Also fails on: :let instance Functor id where { map f x = f x }

trillioneyes commented 10 years ago

My initial implementation of :let was kind of incomplete; I foolishly assumed that no one would want to define a class, instance, or infix declaration at the repl, among other things.

I'm trying to make it work for every kind of declaration, even the ones that don't seem worthwhile to me, but it's proving more difficult than I anticipated. As a first step, I should at least be able to catch those errors and print a message in the REPL instead of falling all the way back to haskell.

trillioneyes commented 10 years ago

1428 should fix both of the named issues, though it's not as complete or robust as I might like.

david-christiansen commented 9 years ago

This is fixed now!