:def shows function definition that pattern-matches on a Type

[RyanGlScott]

Load this into the Idris REPL:

module Bug

data T : Type -> Type where
  MkT : T Bool

f : (x : Type) -> T x -> x
f _ MkT = True

And run :def f:

$ idris Bug.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.0
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
*Bug> :def f
Compiled patterns:
[Case: (x : Type ./Bug.idr.j3) -> Bug.T x -> x []
COMPILE TIME:

[{e_0},{e_1}] case {e_1} of
    Bug.MkT() => Prelude.Bool.True

RUN TIME:

[{e_0},{e_1}] Prelude.Bool.True

Inlinable]
Original definiton:
Bug.f Prelude.Bool.Bool Bug.MkT = Prelude.Bool.True
Total

That definition for f looks suspicious. If you try to actually use it:

module Bug

data T : Type -> Type where
  MkT : T Bool

f : (x : Type) -> T x -> x
f Prelude.Bool.Bool MkT = Prelude.Bool.True

Then Idris will rightfully complain, since you can't pattern-match on Types:

$ idris --check Bug.idr
Bug.idr:7:3:When checking left hand side of f:
No explicit types on left hand side: Bool

[ahmadsalim]

@RyanGlScott As far as I can see it pattern matches on the value on compile time (note {e_1} not {e_0}), and does no pattern matching on runtime.

Although, the error comes too early since this should be a forced pattern.