Mercurial > urweb
comparison src/explify.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 | c7b9a33c26c8 |
children | bb942416bf1c |
comparison
equal
deleted
inserted
replaced
1638:3bf727a08db8 | 1639:6c00d8af6239 |
---|---|
40 | 40 |
41 | L.KUnit => (L'.KUnit, loc) | 41 | L.KUnit => (L'.KUnit, loc) |
42 | L.KTuple ks => (L'.KTuple (map explifyKind ks), loc) | 42 | L.KTuple ks => (L'.KTuple (map explifyKind ks), loc) |
43 | 43 |
44 | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc) | 44 | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc) |
45 | L.KUnif (_, _, ref (SOME k)) => explifyKind k | 45 | L.KUnif (_, _, ref (L.KKnown k)) => explifyKind k |
46 | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc) | 46 | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc) |
47 | L.KTupleUnif (loc, _, ref (SOME k)) => explifyKind k | 47 | L.KTupleUnif (loc, _, ref (L.KKnown k)) => explifyKind k |
48 | L.KTupleUnif _ => raise Fail ("explifyKind: KTupleUnif at " ^ EM.spanToString loc) | 48 | L.KTupleUnif _ => raise Fail ("explifyKind: KTupleUnif at " ^ EM.spanToString loc) |
49 | 49 |
50 | L.KRel n => (L'.KRel n, loc) | 50 | L.KRel n => (L'.KRel n, loc) |
51 | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc) | 51 | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc) |
52 | 52 |
74 | 74 |
75 | L.CTuple cs => (L'.CTuple (map explifyCon cs), loc) | 75 | L.CTuple cs => (L'.CTuple (map explifyCon cs), loc) |
76 | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc) | 76 | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc) |
77 | 77 |
78 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) | 78 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) |
79 | L.CUnif (nl, _, _, _, ref (SOME c)) => explifyCon (ElabEnv.mliftConInCon nl c) | 79 | L.CUnif (nl, _, _, _, ref (L.Known c)) => explifyCon (ElabEnv.mliftConInCon nl c) |
80 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) | 80 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) |
81 | 81 |
82 | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc) | 82 | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc) |
83 | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc) | 83 | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc) |
84 | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc) | 84 | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc) |