Fixes #814

src/Type/Type.hs

@@ -46,7 +46,7 @@ module Type.Type (-- * Types
                   , typeList, typeVector, typeApp, typeRef --, typeNull
                   , typeOptional, typeMakeTuple
                   , typeCCtx, typeCCtxx, typeFieldAddr
-                  , isOptional, makeOptionalType, unOptional
+                  , isOptional, makeOptionalType, unOptional, unImplicit
                   , typeReuse, typeLocal, isTypeLocal
 
                   , tconHandled, tconHandled1, wrapHandledFromDataEffect
@@ -957,6 +957,12 @@ unOptional tp
   = case expandSyn tp of
       TApp (TCon tc) [t] | tc == tconOptional -> t
       _ -> tp
+
+unImplicit :: Type -> Type
+unImplicit tp
+  = case expandSyn tp of
+      TFun args eff res -> TFun (filter (not . isImplicitParamName . fst) args) eff res
+      _ -> tp
 
 -- | Remove type synonym indirections.
 pruneSyn :: Rho -> Rho

src/Type/Unify.hs

@@ -145,10 +145,11 @@ matchArguments matchSome range free tp fixed named mbExpResTp
                         then do subst rho1
                         else unifyError NoMatch
 
-subsumeSubst :: Range -> Tvs -> Type -> Type -> Unify (Type,Rho, Core.Expr -> Core.Expr)
+subsumeSubst :: HasCallStack => Range -> Tvs -> Type -> Type -> Unify (Type,Rho, Core.Expr -> Core.Expr)
 subsumeSubst range free tp1 tp2
   = do stp1 <- subst tp1
        stp2 <- subst tp2
+       -- trace ("subsumeSubst: " ++ show (pretty stp1, pretty stp2)) $ return ()
        subsume range free stp1 stp2
 
 -- | See if two types match exactly up to renaming of free type variables
@@ -186,8 +187,11 @@ subsume range free tp1 tp2
     do -- skolemize,instantiate and unify
        (sks,rho1,core1) <- skolemizeEx range tp1
        (tvs,rho2,core2) <- instantiateEx range tp2
+       -- We can remove the implicit requirements from the type as they will be resolved later
+       -- we just need to know if the "shape" will match after implicits are resolved
+       -- TODO: Should we also unOptional here, instead of in type matching?
        -- trace ("  subsume: " ++ show (pretty rho1, pretty rho2) ++ ", free: " ++ show (map pretty (tvsList free))) $ return ()
-       unify rho2 rho1
+       unify (unImplicit rho2) (unImplicit rho1)
 
        -- escape check: no skolems should escape into the environment
        -- entailment check: predicates should be entailed

test/overload/implicit-positional.kk

@@ -0,0 +1,17 @@
+// Merge sort can be done on any pre-order
+pub fun pre-order/sort(l : list<a>, ?(<=) : (a, a) -> e bool) : e list<a>
+  []
+
+// But a total order also works of course
+pub fun order/sort(l : list<a>, ?cmp : (a, a) -> e order) : e list<a>
+  []
+
+// We can define a left-to-right total order on vectors, if the elements are totally ordered
+pub fun vector/cmp-lr(xs : vector<char>, ys : vector<char>, ?cmp : (char,char) -> e order): e order
+  Gt
+
+// ----- MAIN ------
+pub fun main()
+  val labels = ["abc".vector, "abd".vector]
+  labels.sort(cmp-lr)
+  ()

test/overload/implicit-positional.kk.out

@@ -0,0 +1,6 @@
+overload/implicit-positional/order/sort: forall<a,e> (l : list<a>, ?cmp : (a, a) -> e order) -> e list<a>
+overload/implicit-positional/pre-order/sort: forall<a,e> (l : list<a>, ?(<=) : (a, a) -> e bool) -> e list<a>
+overload/implicit-positional/vector/cmp-lr: forall<e> (xs : vector<char>, ys : vector<char>, ?cmp : (char, char) -> e order) -> e order
+overload/implicit-positional/main: () -> ()
+test/overload/implicit-positional@kk(16, 3): type warning: expression has no effect and is unused
+ hint: did you forget an operator? or used "fun" instead of "fn"?