comparison src/elab_ops.sml @ 1639:6c00d8af6239

Add a new scoping check for unification variables, to fix a type inference bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 11:29:13 -0500
parents 20f898c29525
children d6c45026240d
comparison
equal deleted inserted replaced
1638:3bf727a08db8 1639:6c00d8af6239
154 distribute := 0; 154 distribute := 0;
155 fuse := 0) 155 fuse := 0)
156 156
157 fun hnormCon env (cAll as (c, loc)) = 157 fun hnormCon env (cAll as (c, loc)) =
158 case c of 158 case c of
159 CUnif (nl, _, _, _, ref (SOME c)) => (#1 (hnormCon env (E.mliftConInCon nl c)), loc) 159 CUnif (nl, _, _, _, ref (Known c)) => (#1 (hnormCon env (E.mliftConInCon nl c)), loc)
160 160
161 | CNamed xn => 161 | CNamed xn =>
162 (case E.lookupCNamed env xn of 162 (case E.lookupCNamed env xn of
163 (_, _, SOME c') => hnormCon env c' 163 (_, _, SOME c') => hnormCon env c'
164 | _ => cAll) 164 | _ => cAll)
275 275
276 fun tryIdentity () = 276 fun tryIdentity () =
277 let 277 let
278 fun cunif () = 278 fun cunif () =
279 let 279 let
280 val r = ref NONE 280 val r = ref (Unknown (fn _ => true))
281 in 281 in
282 (r, (CUnif (0, loc, (KType, loc), "_", r), loc)) 282 (r, (CUnif (0, loc, (KType, loc), "_", r), loc))
283 end 283 end
284 284
285 val (vR, v) = cunif () 285 val (vR, v) = cunif ()