address serious problem of type inference (introduced in 6f085332c7d3): _type_constraint_ needs type scheme A --> A with proper scope of parameters, otherwise term "(f :: _ => _) :: 'c => 'c" will get type "'a => 'b", for example;
authorwenzelm
Mon Mar 28 22:44:14 2011 +0200 (2011-03-28)
changeset 42143786ccfffcd67
parent 42142 d24a93025feb
child 42144 15218eb98fd7
address serious problem of type inference (introduced in 6f085332c7d3): _type_constraint_ needs type scheme A --> A with proper scope of parameters, otherwise term "(f :: _ => _) :: 'c => 'c" will get type "'a => 'b", for example;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Mon Mar 28 17:33:16 2011 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Mon Mar 28 22:44:14 2011 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4  
     1.5  (* prepare_term *)
     1.6  
     1.7 -fun prepare_term const_type tm (vparams, params, idx) =
     1.8 +fun prepare_term ctxt const_type tm (vparams, params, idx) =
     1.9    let
    1.10      fun add_vparm xi (ps_idx as (ps, idx)) =
    1.11        if not (Vartab.defined ps xi) then
    1.12 @@ -118,9 +118,12 @@
    1.13  
    1.14      fun prepare (Const ("_type_constraint_", T) $ t) ps_idx =
    1.15            let
    1.16 -            val (T', ps_idx') = prepare_typ T ps_idx;
    1.17 +            fun err () =
    1.18 +              error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
    1.19 +            val A = (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ());
    1.20 +            val (A', ps_idx') = prepare_typ A ps_idx;
    1.21              val (t', ps_idx'') = prepare t ps_idx';
    1.22 -          in (Const ("_type_constraint_", T') $ t', ps_idx'') end
    1.23 +          in (Const ("_type_constraint_", A' --> A') $ t', ps_idx'') end
    1.24        | prepare (Const (c, T)) (ps, idx) =
    1.25            (case const_type c of
    1.26              SOME U =>
    1.27 @@ -344,8 +347,8 @@
    1.28  
    1.29      val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
    1.30      val (ts', (_, _, idx)) =
    1.31 -      fold_map (prepare_term const_type o constrain_vars) ts
    1.32 -      (Vartab.empty, Vartab.empty, 0);
    1.33 +      fold_map (prepare_term ctxt const_type o constrain_vars) ts
    1.34 +        (Vartab.empty, Vartab.empty, 0);
    1.35    in (idx, ts') end;
    1.36  
    1.37  fun infer_types ctxt const_type var_type raw_ts =