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