From 3d3473844a47266f4f2dd6c3f5fccbf8e290bc15 Mon Sep 17 00:00:00 2001 From: Patrick Oscar Boykin Date: Sat, 21 Oct 2023 15:03:13 -1000 Subject: [PATCH] Fix coerce in Infer.subsCheck --- .../scala/org/bykn/bosatsu/rankn/Infer.scala | 27 ++++++++++--------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/core/src/main/scala/org/bykn/bosatsu/rankn/Infer.scala b/core/src/main/scala/org/bykn/bosatsu/rankn/Infer.scala index 8a292a8f5..4ef773a85 100644 --- a/core/src/main/scala/org/bykn/bosatsu/rankn/Infer.scala +++ b/core/src/main/scala/org/bykn/bosatsu/rankn/Infer.scala @@ -492,6 +492,7 @@ object Infer { } yield TypedExpr.coerceFn(a1s, r2, coarg, cores, ks) /* + * If t <:< rho then coerce to rho * invariant: second argument is in weak prenex form, which means that all * the covariant positions have lifted the ForAlls out, e.g. * forall a. a -> (forall b. b -> b) @@ -507,6 +508,7 @@ object Infer { subsCheckRho2(rhot, rho, left, right) } + // if t <:< rho, then coerce to rho def subsCheckRho2(t: Type.Rho, rho: Type.Rho, left: Region, right: Region): Infer[TypedExpr.Coerce] = // get the kinds to make sure they are well kinded kindOf(t, left).product(kindOf(rho, right)) *> @@ -551,7 +553,7 @@ object Infer { // should we coerce to t2? Seems like... but copying previous code _ <- subsCheck(l1, l2, left, right) ks <- checkedKinds - } yield TypedExpr.coerceRho(rho1, ks) + } yield TypedExpr.coerceRho(ta, ks) case (ta@Type.TyApply(l1, r1), rho2) => for { kl <- kindOf(l1, left) @@ -571,8 +573,7 @@ object Infer { } _ <- subsCheck(l1, l2, left, right) ks <- checkedKinds - // should we coerce to t2? Seems like... but copying previous code - } yield TypedExpr.coerceRho(ta, ks) + } yield TypedExpr.coerceRho(rho2, ks) case (t1, t2) => // rule: MONO for { @@ -949,7 +950,7 @@ object Infer { tbranches <- branches.parTraverse { case (p, r) => inferBranch(p, check, r) } - (rho, regRho, resBranches) <- narrowBranches(tbranches) + (rho, regRho, resBranches) <- widenBranches(tbranches) _ <- infer.set((rho, regRho)) } yield TypedExpr.Match(tsigma, resBranches, tag) } @@ -957,34 +958,34 @@ object Infer { } } - def narrowBranches[A: HasRegion](branches: NonEmptyList[(Pattern, (TypedExpr.Rho[A], Type.Rho))]): Infer[(Type.Rho, Region, NonEmptyList[(Pattern, TypedExpr.Rho[A])])] = { + def widenBranches[A: HasRegion](branches: NonEmptyList[(Pattern, (TypedExpr.Rho[A], Type.Rho))]): Infer[(Type.Rho, Region, NonEmptyList[(Pattern, TypedExpr.Rho[A])])] = { - def minBy[M[_]: Monad, B](head: B, tail: List[B])(lteq: (B, B) => M[Boolean]): M[B] = + def maxBy[M[_]: Monad, B](head: B, tail: List[B])(gteq: (B, B) => M[Boolean]): M[B] = tail match { case Nil => Monad[M].pure(head) case h :: tail => - lteq(head, h) + gteq(head, h) .flatMap { keep => val next = if (keep) head else h - minBy(next, tail)(lteq) + maxBy(next, tail)(gteq) } } - def ltEq[K](left: (TypedExpr[A], K), right: (TypedExpr[A], K)): Infer[Boolean] = { + def gtEq[K](left: (TypedExpr[A], K), right: (TypedExpr[A], K)): Infer[Boolean] = { val leftTE = left._1 val rightTE = right._1 val lt = leftTE.getType val lr = region(leftTE) val rt = rightTE.getType val rr = region(rightTE) - // right <= left if left subsumes right - subsCheck(lt, rt, lr, rr) + // left >= right if right subsumes left + subsCheck(rt, lt, rr, lr) .peek .flatMap { case Right(_) => pure(true) case Left(_) => // maybe the other way around - subsCheck(rt, lt, rr, lr) + subsCheck(lt, rt, lr, rr) .peek .flatMap { case Right(_) => @@ -1000,7 +1001,7 @@ object Infer { val withIdx = branches.zipWithIndex.map { case ((p, (te, tpe)), idx) => (te, (p, tpe, idx)) } for { - (minRes, (minPat, resTRho, minIdx)) <- minBy(withIdx.head, withIdx.tail)((a, b) => ltEq(a, b)) + (minRes, (minPat, resTRho, minIdx)) <- maxBy(withIdx.head, withIdx.tail)((a, b) => gtEq(a, b)) resRegion = region(minRes) resBranches <- withIdx.parTraverse { case (te, (p, tpe, idx)) => if (idx != minIdx) {