Correct chasing of type variable instantiations during type unification.
authorpaulson
Wed Sep 23 11:05:28 2009 +0100 (2009-09-23)
changeset 32648143e0b0a6b33
parent 32597 1e2872252f91
child 32649 442e03154ee6
Correct chasing of type variable instantiations during type unification.
The following theory should not raise exception TERM:

constdefs
somepredicate :: "(('b => 'b) => ('a => 'a))
=> 'a => 'b => bool"
"somepredicate upd v x == True"

lemma somepredicate_idI:
"somepredicate id (f v) v"
by (simp add: somepredicate_def)

lemma somepredicate_triv:
"somepredicate upd v x ==> somepredicate upd v x"
by assumption

lemmas somepredicate_triv [OF somepredicate_idI]

lemmas st' = somepredicate_triv[where v="h :: nat => bool"]

lemmas st2 = st'[OF somepredicate_idI]
src/Pure/envir.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/envir.ML	Thu Sep 17 15:04:46 2009 +0100
     1.2 +++ b/src/Pure/envir.ML	Wed Sep 23 11:05:28 2009 +0100
     1.3 @@ -282,12 +282,9 @@
     1.4    let
     1.5      val funerr = "fastype: expected function type";
     1.6      fun fast Ts (f $ u) =
     1.7 -          (case fast Ts f of
     1.8 +          (case Type.devar tyenv (fast Ts f) of
     1.9              Type ("fun", [_, T]) => T
    1.10 -          | TVar v =>
    1.11 -              (case Type.lookup tyenv v of
    1.12 -                SOME (Type ("fun", [_, T])) => T
    1.13 -              | _ => raise TERM (funerr, [f $ u]))
    1.14 +          | TVar v => raise TERM (funerr, [f $ u])
    1.15            | _ => raise TERM (funerr, [f $ u]))
    1.16        | fast Ts (Const (_, T)) = T
    1.17        | fast Ts (Free (_, T)) = T
     2.1 --- a/src/Pure/type.ML	Thu Sep 17 15:04:46 2009 +0100
     2.2 +++ b/src/Pure/type.ML	Wed Sep 23 11:05:28 2009 +0100
     2.3 @@ -55,6 +55,7 @@
     2.4    exception TYPE_MATCH
     2.5    type tyenv = (sort * typ) Vartab.table
     2.6    val lookup: tyenv -> indexname * sort -> typ option
     2.7 +  val devar: tyenv -> typ -> typ
     2.8    val typ_match: tsig -> typ * typ -> tyenv -> tyenv
     2.9    val typ_instance: tsig -> typ * typ -> bool
    2.10    val raw_match: typ * typ -> tyenv -> tyenv