Wrong shallow embedding for abstract polymorphic functions.

[gteege]

The shallow embedding generated by --shallow-desugar-tuples is wrong when there are "hidden" type parameters in terms, even if the type is specified in Cogent. Example:

a1 : all(t). t -> ()
a2 : all(t). () -> t
f : () -> ()
f() = a1[U32](a2[U32]())
g : () -> ()
g () = f ()

When the shallow embedding is loaded into isabelle based on session CogentShallow the following error message is caused:

Loading theory "Abspoly-ShallowTuples.Abspoly_Shallow_Desugar_Tuples"
### Additional type variable(s) in specification of "f": 'a
### theory "Abspoly-ShallowTuples.Abspoly_Shallow_Desugar_Tuples"
### 0.033s elapsed time, 0.060s cpu time, 0.000s GC time
*** Type unification failed: Clash of types "unit" and "_ itself"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  f :: ??'a itself \<Rightarrow> unit \<Rightarrow> unit
*** Operand:   () :: unit
*** 
*** At command "definition" (line 15 of "~/work/projekte/code/HoBit/devel/experiments/cogent_shallow_error/Abspoly_Shallow_Desugar_Tuples.thy")

The reason is that the type for type parameter t cannot be inferred by Isabelle because there is no relation to other types. Thus t remains as an implicit type variable in the body of f and causes the shallow embedding of f to be polymorphic. In Cogent the type to be used is explicitly specified as U32, however, this information is not transferred to the shallow embedding.

I can see two possible solutions:

• transfer the type determined by Cogent to the shallow embedding. (Is it possible to specify the type to be used in Isabelle, if both a1 and a2 are declared as polymorphic consts?) This should only be done in situations where it is required. This means that the shallow embedding can only be generated after the typechecking, when all types are known.
• monomorphisize all abstract polymorphic functions in the shallow embedding, as it is done in the embedding generated by --shallow-desugar. The drawback is that the user has to specify properties and proofs for all instances of the abstract functions seperately, instead of once for the polymorphic function.