Type providers must build one of these in an IO computation.
- Provide : (x : a) ->
Return a term to be spliced in
the term to be spliced (i.e. the proof)
- Error : (msg : String) ->
Report an error to the user and stop compilation
the error message