search

idris-lang / Idris-dev

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

Quasiquoting a number literal gives `No such variable qquoteTy` #2269

Open LeifW opened 9 years ago

LeifW commented 9 years ago

e.g. `(5) I can imagine this being problematic with these being interpreted through fromIntegral?

I can't find anything by that name in libs/prelude/Language/Reflection.idr; I do find a quotedTy in there. Looking in src/Idris/Elab/Term.hs I see a few other identifiers in strings that don't seem to be present in libs.

david-christiansen commented 9 years ago

The problem here is that quasiquotation is a bit like the REPL - there's no type information available, because you can quote any type. So internally, it makes a hidden variable called qquoteTy to represent the type of the contained term until it's solved. In this case, it couldn't solve it.

I agree that this error message is garbage. I'll try to think about how to make it say "Couldn't infer type of quoted term 'fromInteger 5', consider giving an explicit goal type." instead.

In the meantime, do as my mythical error message suggested and give a goal type. That looks like (5 : Integer)` or(5 : Nat)`. Then, Idris has a type to work with and doesn't need to guess.