"Safe" axiomatization

[lastland]

Issue by sweirich
Tuesday Jun 25, 2019 at 10:43 GMT
Originally opened as antalsz/hs-to-coq#127

---

It would be good if hs-to-coq could help distinguish whether added axioms are trivially safe or not. i.e.

Axiom bad : forall {a}, a.

vs

Axiom ok: forall {a}, {Default a} -> a.
Axiom isUpper : Char -> bool.
Axiom newtype : Type.        
Instance Default_newtype : Default newtype.
Axiom str2new : String -> newtype.   

The only tricky bit is that we have to approximate whether types are inhabited (i.e. whether default instances are available).

But it would good to be able to see in the edits file which axioms need more scrutiny.