Substitution into default arguments, using a WIP compiler patch: https://github.com/tpsinnem/Idris-dev/tree/default-arg-subst . UPDATE: Now works in syntax rules as well: https://gist.github.com/tpsinnem/9970467

gistfile1.txt

%default total

--------------------------------------------------------------------------
--  First some generic stuff that will probably also be useful elsewhere:
--------------------------------------------------------------------------

DecProofType : {a:Type} -> Dec a -> Type
DecProofType {a} (Yes _)  = a
DecProofType {a} (No _)   = a -> _|_

decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
decProof (Yes x)  = x
decProof (No x)   = x

-------------------------------------------------------------------------------
--  A function using the new substitution-into-default-argument functionality:
-------------------------------------------------------------------------------

data Hooray : Type where
  hooray : Hooray

sameHooray : (n:Nat) -> (m:Nat) -> 
             {default (decProof (decEq n m)) p : (n = m)} -> Hooray
sameHooray _ _ = hooray

--------------------------------
--  Poking at this in the REPL:
--------------------------------

{-

*DecProofExample> sameHooray Z Z
hooray : Hooray

*DecProofExample> sameHooray Z (S Z)
(input):1:12:When elaborating argument p to function Main.sameHooray:
        Can't unify
                DecProofType dec
        with
                0 = 1
                                                        
        Specifically:
                Can't unify
                        DecProofType dec
                with
                        0 = 1

-}

-------------
--  Success!
-------------