search

idris-lang / Idris-dev

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

Implicit variables show up in types of holes even when not pattern matched #2750

Open enolan opened 8 years ago

enolan commented 8 years ago 
data Foo : Type where
  MkFoo : Int -> {a : Nat} -> Foo

bar : Foo -> Foo -> Nat
bar (MkFoo x) (MkFoo y) = ?bar_rhs_2

If we ask the type of bar_rhs_2:

$ .cabal-sandbox/bin/idris ~/junk/newbug.idr                                                                                                                                                                         
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 0.9.19.1-git:06edf43
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Holes: Main.bar_rhs_2
*/home/enolan/junk/newbug> :t bar_rhs_2
  x : Int
  y : Int
  a : Nat
  a1 : Nat
--------------------------------------
bar_rhs_2 : Nat
Holes: Main.bar_rhs_2

Both implicit variables are shown, even though they can't actually be used. They're available in a sense, but this is at least confusing.

ahmadsalim commented 8 years ago

I think that this should be on when showimplicts is enabled, but otherwise should be disabled as suggested. Perhaps, even then it might be nice if it was somehow marked as implicit e.g. {a : Nat} instead of shown as an explicit variable.