idris-0.9.17.1: test/proof007/DefaultArgUnknownName.idr
module DefaultArgUnknownName
-- FIXME: What is the expected behaviour here? Should the type declaration
-- not compile?
funWithBadDefArg : { default sadgjhsag arg : () } -> ()
funWithBadDefArg = ()
test : ()
test = funWithBadDefArg