ArtificialConstraint.idr

interface Parseable a where
  parse : String -> a

data Name : Type where
  MkName : String -> Name

Parseable Name where
  parse = MkName

data A : Type -> Type where
  MkA : Parseable a => (a -> a) -> A a

f : Name -> Name

read : String -> A t -> t
read s (MkA f) = parse s

Using it:

*ArtificialConstraint> :let arg = MkA f
Holes: Main.f
*ArtificialConstraint> read "asdas" arg
MkName "asdas" : Name
Holes: Main.f