(* The example from the 'Higher-order polymorphim' subsection of \cite[p. 66--67]{KennedyThesis}.
 *)
;

(*[ val polyadd : (-all d1, d2 : dim- real(d1) -> real(d2) -> real(d1 * d2)) -> real(KG) ]*)
fun polyadd prod =
  prod 2.0 KG + prod KG 3.0