diff options
| -rw-r--r-- | src/elaborate.sml | 23 | ||||
| -rw-r--r-- | tests/functor.lac | 5 |
2 files changed, 26 insertions, 2 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 9c96060d..5e0ba5fc 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -396,6 +396,17 @@ val subConInCon = bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) | (ctx, _) => ctx} +fun subStrInSgn (m1, m2) = + U.Sgn.map {kind = fn k => k, + con = fn c as L'.CModProj (m1', ms, x) => + if m1 = m1' then + L'.CModProj (m2, ms, x) + else + c + | c => c, + sgn_item = fn sgi => sgi, + sgn = fn sgn => sgn} + type record_summary = { fields : (L'.con * L'.con) list, unifs : (L'.con * L'.con option ref) list, @@ -1241,8 +1252,16 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) = end | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => - (subSgn env dom2 dom1; - subSgn env ran1 ran2) + let + val ran1 = + if n1 = n2 then + ran1 + else + subStrInSgn (n1, n2) ran1 + in + subSgn env dom2 dom1; + subSgn (E.pushStrNamedAs env m2 n2 dom2) ran1 ran2 + end | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) diff --git a/tests/functor.lac b/tests/functor.lac index 7d2983e0..6e19603d 100644 --- a/tests/functor.lac +++ b/tests/functor.lac @@ -13,3 +13,8 @@ functor F (M : S) : T where type t = M.t = struct type t = M.t val three = M.s (M.s (M.s M.z)) end + +structure F2 : functor (M : S) : T where type t = M.t = F +structure F3 : functor (M : S) : T = F +(*structure F4 : functor (M : S) : sig type q end = F*) +(*structure F5 : functor (M : S) : T where type t = int = F*) |