| Prim (f, al) ->
      let tf : texp = find_type_var f.name env in
      let t0 = tvar() in
      let rec targs = function
          [] -> t0, [ ]
        | a:: rest ->
            let tr, sr = targs rest in
            let tl, sl = infer (subst_tenv sr env) a in
            Tarrow (tl, tr), compose sl sr in
      let t, s = targs al in
      let s1 = unify (subst_texp s tf) t in
      let s2 = compose s1 s in
      subst_texp s2 t0, s2