assume untyped parameters live in Type (fix #111)

_CoqProject

@@ -49,6 +49,7 @@ Coq2020_material/CoqWS_expansion/withoutHB.v
 
 tests/type_of_exported_ops.v
 tests/duplicate_structure.v
+tests/instance_params_no_type.v
 
 -R . HB
 

hb.elpi

@@ -1087,7 +1087,9 @@ main-mixin-requires Str GR GRFS [From|PO] SN :- !, std.do! [
 % be [] at call site.
 pred postulate-arity i:arity, i:list term, i:term, o:term, o:term.
 postulate-arity (parameter ID _ S A) Acc T T1 Ty :-
+  std.assert-ok! (coq.typecheck-ty S _) "arity parameter illtyped",
   if-verbose (coq.say "HB: postulating" ID),
+  if (var S) (coq.fresh-type S) true,
   @local! => coq.env.add-const ID _ S @opaque! C,
   Var = global (const C),
   postulate-arity (A Var) [Var|Acc] T T1 Ty.
@@ -1831,6 +1833,7 @@ process-asset-named-parameters (asset-parameter Name _ Rest as R) D Module Param
 process-asset-named-parameters (asset-parameter Name T Rest) D Module Params :- std.do! [
   std.assert-ok! (coq.typecheck-ty T _) "Illtyped parameter",
   if-verbose (coq.say "HB: postulate " Name),
+  if (var T) (coq.fresh-type T) true,
   @local! => coq.env.add-const Name _ T @opaque! C, % no body, local -> a variable
   TheParam = global (const C),
   process-asset-named-parameters (Rest TheParam) D Module [pr TheParam T|Params],

tests/instance_params_no_type.v

@@ -0,0 +1,7 @@
+From HB Require Import structures.
+
+HB.mixin Record is_foo P A := { op : P -> A -> A }.
+HB.structure Definition foo P := { A of is_foo P A }.
+
+Axiom f : forall T, T -> nat -> nat.
+HB.instance Definition bar P := is_foo.Build P nat (f P).