improvement on the typechecker

src/compiler/api/GF/Compile/Compute/Concrete2.hs

@@ -4,11 +4,11 @@ module GF.Compile.Compute.Concrete2
            (Env, Scope, Value(..), Variants(..), Constraint, OptionInfo(..), ChoiceMap, cleanOptions,
             ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM,
             mapVariants, unvariants, variants2consts, consts2variants,
-            runEvalM, runEvalMWithOpts, stdPredef, globals,
+            runEvalM, runEvalMWithOpts, stdPredef, globals, withState,
             PredefImpl, Predef(..), ($\),
             pdCanonicalArgs, pdArity,
             normalForm, normalFlatForm,
-            eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect,
+            eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect, State(..),
             newResiduation, getMeta, setMeta, MetaState(..), variants, try,
             evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where
 
@@ -727,6 +727,9 @@ runEvalMWithOpts g cs (EvalM f) = Check $ \(es,ws) ->
   where
     init = State cs Map.empty []
 
+withState :: State -> EvalM a -> EvalM a
+withState state (EvalM f) = EvalM $ \g k _ r ws -> f g k state r ws
+
 reset :: EvalM a -> EvalM [a]
 reset (EvalM f) = EvalM $ \g k state r ws ->
   case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of
@@ -764,12 +767,11 @@ variants' c f xs = EvalM (\g k state@(State choices metas opts) r msgs ->
                      Fail    msg msgs -> Fail msg msgs
                      Success ts  msgs -> backtrack g (j+1) xs choices metas opts ts msgs
 
-try :: (a -> EvalM b) -> [a] -> Message -> EvalM b
-try f xs msg = EvalM (\g k state r msgs ->
+try :: (a -> EvalM b) -> ([(b,State)] -> EvalM b) -> [a] -> EvalM b
+try f select xs = EvalM (\g k state r msgs ->
   let (res,msgs') = backtrack g xs state [] msgs
-  in case res of
-       []  -> Fail msg msgs'
-       res -> continue g k res r msgs')
+  in case select res of
+       EvalM f' -> f' g k state r msgs')
   where
     backtrack g []     state res msgs = (res,msgs)
     backtrack g (x:xs) state res msgs =
@@ -778,12 +780,6 @@ try f xs msg = EvalM (\g k state r msgs ->
                      Fail msg _       -> backtrack g xs state res msgs
                      Success res msgs -> backtrack g xs state res msgs
 
-    continue g k []              r msgs = Success r msgs
-    continue g k ((x,state):res) r msgs =
-      case k x state r msgs of
-        Fail msg msgs  -> Fail msg msgs
-        Success r msgs -> continue g k res r msgs
-
 newResiduation :: Scope -> EvalM MetaId
 newResiduation scope = EvalM (\g k (State choices metas opts) r msgs ->
   let meta_id = Map.size metas+1

src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs

@@ -470,8 +470,9 @@ resolveOverloads scope c t0 q args mb_ty = do
                           (c2,c3)  = split c23
                       arg_tys <- mapCM (checkArg g) c1 args
                       let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys
-                      try (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) v_ttys (pp "Overload resolution failed")
-                      
+                      try (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty)
+                          (\ttys -> fmap (\(ts,ty) -> (FV ts,ty)) (snd (minimum g ttys)))
+                          v_ttys
   where
     checkArg g c (ImplArg arg) = do
       let (c1,c2) = split c
@@ -484,6 +485,46 @@ resolveOverloads scope c t0 q args mb_ty = do
       let v = eval g (scopeEnv scope) c2 arg []
       return (arg,v,arg_ty)
 
+    minimum g []                    = (maxBound,err)
+      where
+        err = evalError (pp "Overload resolution failed")
+    minimum g (tty@((t,ty),state):ttys) =
+      let ty'      = zonk ty
+          a        = arity ty'
+          (a',res) = minimum g ttys
+      in case compare a a' of
+           GT -> (a',res)
+           EQ -> (a',join t ty' state res)
+           LT -> (a ,one  t ty' state)
+      where
+        arity :: Value -> Int
+        arity (VProd _ _ _ ty) = 1 + arity ty
+        arity _                = 0
+
+        zonk :: Value -> Value
+        zonk (VProd bt x ty1 ty2) = VProd bt x (zonk ty1) (zonk ty2)
+        zonk (VMeta i vs)         =
+          case Map.lookup i (metaVars state) of
+            Just (Bound _ v)              -> zonk (apply g v vs)
+            Just (Residuation _ (Just v)) -> zonk (apply g v vs)
+            _                             -> VMeta i (map zonk vs)
+        zonk (VSusp i k vs)      =
+          case Map.lookup i (metaVars state) of
+            Just (Bound _ v)              -> zonk (apply g (k v) vs)
+            Just (Residuation _ (Just v)) -> zonk (apply g (k v) vs)
+            _                             -> VSusp i k (map zonk vs)
+        zonk v                   = v
+
+        one t ty state = do
+          t <- withState state (zonkTerm [] t)
+          return ([t],ty)
+
+        join t ty state res = do
+          t <- withState state (zonkTerm [] t)
+          (ts,ty') <- res
+          unify scope ty ty'
+          return (t:ts,ty)
+
 reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho)
 reapply2 scope c fun fun_ty []                                mb_ty = instSigma scope c fun fun_ty mb_ty
 reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case