Fix the typing of functions. One needs to call type_check_branches with argument precise = true

precise = false returns the constraint itself as output type (which is not sound when it is a variable).

tests/poly/part2.cd

@@ -24,6 +24,7 @@ let max (x : 'a) (y : 'a) : 'a = if x >> y then x else y;;
 
 max 42;;
 
+
 type RBtree = Btree | Rtree
 type Btree  = <blk elem='a>[ RBtree RBtree ] | []
 type Rtree  = <red elem='a>[ Btree  Btree ]
@@ -40,3 +41,18 @@ let balance ( Unbal ->Rtree ; ('b \ Unbal) ->('b \ Unbal) )
       -> <red (y)>[  <blk (x)>[ a b ]   <blk (z)>[ c d ]  ]
   | x -> x
 ;;
+
+let balance (Unbal ->Rtree ;  'a -> 'a )
+  | <blk (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
+  | <blk (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ]
+  | <blk (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ]
+  | <blk (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ]
+      -> <red (y)>[  <blk (x)>[ a b ]   <blk (z)>[ c d ]  ]
+  | x -> x
+;;
+let r = balance <blk elem=1>[ <red elem=1>[ <red elem=1>[ 1 2] 3 ]4];;
+let id ('a -> 'a)
+    Int  -> "foo"
+  | x -> x
+;;
+id 42;;

typing/typer.ml

@@ -911,8 +911,12 @@ and type_check' loc env ed constr precise = match ed with
           let acc = a.fun_body.br_accept in
           if not (Types.subtype t1 acc) then
             raise_loc loc (NonExhaustive (Types.diff t1 acc));
-          let t = type_check_branches loc env t1 a.fun_body t2 false in
+          let t = type_check_branches loc env t1 a.fun_body t2 true in
+          try
             (Types.squaresubtype env.delta t t2)::tacc (* H_j *)
+          with
+            Types.Tallying.UnSatConstr _ ->
+              raise_loc loc (Constraint (t, t2))
         ) [] a.fun_iface
       in
       List.iter (fun sl ->