[isabelle] Code generation with type classes leads to compile error



Hello,

I ran into a case where the code generation produces invalid ML code (with the default code generator setup).

The problem seems to be related to ML code for type classes which under certain circumstances leads to a polymorphic value (instead of a polymorphic function) for representation of the type class. And polymorphic values aren't really polymorphic in ML. The attached theory shows this. (Tested with 2019-RC0)

It gives an error as follows:


   Error: Type mismatch in type constraint.
       Value: {uniformity = uniformity_lista} : {uniformity: 'a}
       Constraint: 'a list uniformity
       Reason:
          Can't unify 'a to ('a list * 'a list) filter
             (Type variable is free in surrounding scope)
   {uniformity = uniformity_lista} : 'a list uniformity
   At (line 15 of "generated code")
   Exception- Fail "Static Errors" raised

How can I change my code setup so that the code compiles? (Without changing the class hierarchy.)

Best wishes,
Dominique.


theory Scratch
  imports HOL.Topological_Spaces
begin

(* This is nonsense mathematically, just for the sake of a minimal example *)
instantiation list :: (type) uniformity begin
(* In a real life situation, this is not executable, thus [code del] *)
definition [code del]: "uniformity_list = (Filter.principal {([],[])} :: (('a list)*('a list)) filter)"
instance ..
end

definition "func (x::'a::uniformity) = True"
definition "prog = func [True]"
export_code prog in SML file_prefix xxx

value prog

(* "value prog" fails with:

Error: Type mismatch in type constraint.
   Value: {uniformity = uniformity_lista} : {uniformity: 'a}
   Constraint: 'a list uniformity
   Reason:
      Can't unify 'a to ('a list * 'a list) filter
         (Type variable is free in surrounding scope)
{uniformity = uniformity_lista} : 'a list uniformity
At (line 15 of "generated code")
Exception- Fail "Static Errors" raised

*)

end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.