Fixed polarity error when solving constraints involving optionals.

actonlang · Jan 8, 2024 · a35fcc4 · a35fcc4
1 parent 505f605
commit a35fcc4
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/compiler/Acton/Solver.hs b/compiler/Acton/Solver.hs
@@ -234,7 +234,7 @@ rank env (Cast _ t1@(TVar _ v1) t2@(TVar _ v2))
 rank env (Cast _ t1@TVar{} (TOpt _ t2@TVar{}))
   | univar (tvar t1), univar (tvar t2)      = RVar t1 [t2]
 rank env (Cast _ t1@TVar{} (TOpt _ t2))
-  | univar (tvar t1)                        = RTry t1 (allBelow env t2 ++ [tOpt tWild, tNone]) False
+  | univar (tvar t1)                        = RTry t1 ([tOpt tWild, tNone] ++ allBelow env t2) False
 rank env (Cast _ TNone{} t2@TVar{})
   | univar (tvar t2)                        = RTry t2 [tOpt tWild, tNone] True
 rank env (Cast _ t1@TVar{} t2)

diff --git a/compiler/Acton/Types.hs b/compiler/Acton/Types.hs
@@ -899,7 +899,9 @@ genEnv env cs te ds
                                                  ds1 = map (abstract q ds ws eq1) ds
                                              --traceM ("## genEnv defs 3 [" ++ prstrs gen_vs ++ "]\n" ++ render (nest 6 $ pretty te1))
                                              return (fix_cs, te1, eq2, ds1)
-  | otherwise                           = return (cs, te, [], ds)
+  | otherwise                           = do --traceM ("## genEnv local\n" ++ render (nest 6 $ pretty te))
+                                             --traceM ("## genEnv local cs:\n" ++ render (nest 4 $ vcat $ map pretty cs))
+                                             return (cs, te, [], ds)
   where
     qualify vs cs                       = let (q,wss) = unzip $ map qbind vs in (q, concat wss)
       where qbind v                     = (Quant v (casts ++ impls), wits)