:printdef outputs invalid code

[enolan]

If I take this example from the theorem proving tutorial

disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p ()
  where
    disjointTy : Nat -> Type
    disjointTy Z = ()
    disjointTy (S k) = Void

and put it in a file, then run :printdef disjoint, I get:

*experiment> :printdef disjoint 
disjoint : (n : Nat) -> (0 = S n) -> Void
disjoint n p = replace p ()

If I then replace the original definition with the output of :printdef, I get a type error:

Type checking /home/enolan/junk/experiment.idr
/home/enolan/junk/experiment.idr:9:10:
When elaborating right hand side of disjoint:
Can't unify
        (\{mv0} => ()) (S n) (Type of replace p ())
with
        Void (Expected type)

showimplicits is set off. IMO Idris should only omit implicits in pretty-printed code when the solver outputs the same code as is already in the AST i.e. they should be omitted only when doing so is purely cosmetic.

Tested on HEAD and 0.9.17.

[david-christiansen]

This would be nice! It should also really be showing the contents of the where block. I've basically implemented :printdef by adding support for language features as I need them :-)