{-# LANGUAGE CPP             #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections   #-}

module Infernu.Infer
    ( runTypeInference
    , test
    , Pretty(..)
    , pretty
    , getAnnotations
    , minifyVars
    , TypeError
    )
    where


import           Control.Monad      (foldM, forM)
import qualified Data.Graph.Inductive as Graph
import           Data.Map.Lazy      (Map)
import qualified Data.Map.Lazy      as Map
import           Data.Maybe         (mapMaybe)
import           Data.Set           (Set)
import qualified Data.Set           as Set
import           Prelude            hiding (foldr, mapM, sequence)

import           Data.List          (intercalate)

import           Infernu.Prelude
import qualified Infernu.Builtins.Operators   as Operators
import           Infernu.InferState
import           Infernu.Lib        (safeLookup)
import           Infernu.Log
import           Infernu.Pretty
import           Infernu.Types
import           Infernu.Unify      (unify, unifyAll, unifyPending, unifyPredsL, unifyRowPropertyBiased, unifyl)



getQuantificands :: TypeScheme -> [TVarName]
getQuantificands (TScheme tvars _) = tvars

getAnnotations :: Exp a -> [a]
getAnnotations = foldr (:) []

----------------------------------------------------------------------

closeRowList :: TRowList Type -> TRowList Type
closeRowList (TRowProp n t rest) = TRowProp n t (closeRowList rest)
closeRowList (TRowEnd _) = TRowEnd Nothing
-- TODO: Handle TRowRec, by defining a new named type in which all row types within are closed (recursively).

-- | Replaces a top-level open row type with the closed equivalent.
-- >>> pretty $ closeRow (Fix $ TRow $ TRowProp "a" (schemeEmpty $ Fix $ TRow $ TRowProp "aa" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd (Just $ RowTVar 1))) (TRowEnd (Just $ RowTVar 2)))
-- "{a: {aa: Number, ..b}}"
-- >>> pretty $ closeRow (Fix $ TFunc [Fix $ TRow $ TRowProp "a" (schemeEmpty $ Fix $ TRow $ TRowProp "aa" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd Nothing)) (TRowEnd Nothing)] (Fix $ TBody TString))
-- "{a: {aa: Number}}.(() -> String)"
-- >>> pretty $ closeRow (Fix $ TFunc [Fix $ TRow $ TRowProp "a" (schemeEmpty $ Fix $ TRow $ TRowProp "a.a" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd (Just $ RowTVar 1))) (TRowEnd (Just $ RowTVar 2))] (Fix $ TBody TString))
-- "{a: {a.a: Number, ..b}, ..c}.(() -> String)"
closeRow :: Type -> Type
closeRow (Fix (TRow r)) = Fix . TRow $ closeRowList r
closeRow t = t

----------------------------------------------------------------------


-- For efficiency reasons, types list is returned in reverse order.
accumInfer :: TypeEnv -> [Exp Source] -> Infer [(QualType, Exp (Source, QualType))]
accumInfer env =
  do traceLog ("accumInfer: env: " ++ pretty env)
     foldM accumInfer' []
     where accumInfer' types expr =
             do (t, e) <- inferType env expr
                return ((t,e):types)

inferType  :: TypeEnv -> Exp Source -> Infer (QualType, Exp (Source, QualType))
inferType env expr = do
  traceLog (">> " ++ pretty expr ++ " -- env: " ++ pretty env)
  (t, e) <- inferType' env expr
  unifyPending
  s <- getMainSubst
  st <- getState
  traceLog (">> " ++ pretty expr ++ " -- inferred :: " ++ pretty (applySubst s t))
  traceLog ("   infer state: " ++ prettyTab 3 st)
  return (applySubst s t, fmap (applySubst s) e)

inferType' :: TypeEnv -> Exp Source -> Infer (QualType, Exp (Source, QualType))
inferType' _ (ELit a lit) = do
  let t = Fix $ TBody $ case lit of
                    LitNumber _ -> TNumber
                    LitBoolean _ -> TBoolean
                    LitString _ -> TString
                    LitRegex{} -> TRegex
                    LitUndefined -> TUndefined
                    LitNull -> TNull
  return (qualEmpty t, ELit (a, qualEmpty t) lit)
inferType' env (EVar a n) =
  do t <- instantiateVar a n env
     return (t, EVar (a, t) n)
inferType' env (EAbs a argNames e2) =
  do argTypes <- forM argNames (const $ Fix . TBody . TVar <$> fresh)
     env' <- foldM (\e (n, t) -> addVarScheme e n $ schemeEmpty t) env $ zip argNames argTypes
     (t1, e2') <- inferType env' e2
     pred' <- unifyPredsL a $ qualPred t1
     let t = TQual pred' $ Fix $ TFunc argTypes (qualType t1)
     return (t, EAbs (a, t) argNames e2')
inferType' env (EApp a e1 eArgs) =
  do tvar <- Fix . TBody . TVar <$> fresh
     (t1, e1') <- inferType env e1
     traceLog $ "EApp: Inferred type for func expr: " ++ pretty t1
     argsTE <- accumInfer env eArgs
     traceLog $ "EApp: Inferred types for func args: " ++ intercalate ", " (map pretty argsTE)
     let rargsTE = reverse argsTE
         tArgs = map fst rargsTE
         eArgs' = map snd rargsTE
         preds = concatMap qualPred $ t1:tArgs
     unify a (qualType t1) (Fix $ TFunc (map qualType tArgs) tvar)
     traceLog $ "Inferred preds: " ++ intercalate ", " (map pretty preds)
     tvar' <- do  pred' <- unifyPredsL a preds
                  tvarSubsted <- applyMainSubst tvar
                  return $ TQual pred' tvarSubsted
     traceLog ("Inferred func application: " ++ pretty tvar')
     return (tvar', EApp (a, tvar') e1' eArgs')
inferType' env (ENew a e1 eArgs) =
  do (t1, e1') <- inferType env e1
     argsTE <- accumInfer env eArgs
     thisT <- Fix . TBody . TVar <$> fresh
     resT <- Fix . TBody . TVar <$> fresh
     let rargsTE = reverse argsTE
         tArgs = thisT : map (qualType . fst) rargsTE
         eArgs' = map snd rargsTE
         preds = concatMap qualPred $ t1 : map fst argsTE
     unify a (qualType t1) (Fix $ TFunc tArgs resT)
     -- constrain 'this' to be a row type:
     rowConstraintVar <- RowTVar <$> fresh
     unify a (Fix . TRow . TRowEnd $ Just rowConstraintVar) thisT
     -- close the row type
     resolvedThisT <- applyMainSubst thisT -- otherwise closeRow will not do what we want.
     unify a thisT (closeRow resolvedThisT)
     -- TODO: If the function returns a row type, it should be the resulting type; other it should be 'thisT'
     preds' <- unifyPredsL a preds
     let thisT' = TQual preds' thisT
     return (thisT', ENew (a, thisT') e1' eArgs')
inferType' env (ELet a n e1 e2) =
  do recType <- Fix . TBody . TVar <$> fresh
     recEnv <- addVarScheme env n $ schemeEmpty recType
     (t1, e1') <- inferType recEnv e1
     unify a (qualType t1) recType
     t' <- generalize e1 env t1
     env' <- addVarScheme env n t'
     (t2, e2') <- inferType env' e2
     preds' <- unifyPredsL a $ concatMap qualPred [t1, t2]
     let resT = TQual preds' $ qualType t2
     return (resT, ELet (a, resT) n e1' e2')
-- | Handling of mutable variable assignment.
-- | Prevent mutable variables from being polymorphic.
inferType' env expr@(EAssign a n expr1 expr2) =
  do traceLog $ "EAssign: " ++ pretty expr
     lvalueScheme <- getVarScheme a n env `failWithM` throwError a ("Unbound variable: " ++ show n ++ " in assignment " ++ pretty expr1)
     traceLog $ "EAssign lvalueScheme: " ++ pretty lvalueScheme
     lvalueT <- instantiate lvalueScheme
     (rvalueT, expr1') <- inferType env expr1
     unify a (qualType lvalueT) (qualType rvalueT)
     (tRest, expr2') <- inferType env expr2
     traceLog $ "EAssign lvalueT: " ++ pretty lvalueT
     traceLog $ "EAssign Invoking unifyAllInstances on scheme: " ++ pretty lvalueScheme
     instancePreds <- unifyAllInstances a $ getQuantificands lvalueScheme
     preds <- unifyPredsL a $ concat $ (instancePreds:) $ map qualPred [lvalueT, rvalueT, tRest] -- TODO should update variable scheme
     -- update the variable scheme, removing perhaps some quantified tvars
     varId <- getVarId n env `failWith` throwError a ("Unbound variable: '" ++ show n ++ "'")
     updatedScheme <- generalize expr1 env (schemeType lvalueScheme)
     _ <- setVarScheme env n updatedScheme varId
     --
     let tRest' = TQual preds $ qualType tRest
     return (tRest', EAssign (a, tRest') n expr1' expr2')
inferType' env (EPropAssign a objExpr n expr1 expr2) =
  do (objT, objExpr') <- inferType env objExpr
     (rvalueT, expr1') <- inferType env expr1
     rowTailVar <- RowTVar <$> fresh
     let rvalueScheme = schemeFromQual rvalueT -- generalize expr1 env rvalueT
         rank0Unify = unify a (qualType objT) $ Fix . TRow $ TRowProp n rvalueScheme $ TRowEnd (Just rowTailVar)
     case unFix (qualType objT) of
       TRow trowList ->
         case Map.lookup n . fst $ flattenRow trowList of
          -- lvalue is known to be a property with some scheme
          Just lvalueScheme ->
            do generalizedRvalue <- generalize expr1 env rvalueT
               unifyRowPropertyBiased a rank0Unify (lvalueScheme, generalizedRvalue)
          Nothing -> rank0Unify
       _ -> rank0Unify
     (expr2T, expr2') <- inferType env expr2 -- TODO what about the pred
     --traceLog "EPropAssign - applying unifyAllInstances"
     --instancePred <- unifyAllInstances a [getRowTVar rowTailVar]
     preds <- unifyPredsL a $ concatMap qualPred [objT, rvalueT, expr2T] -- TODO review
     let tRes = TQual preds $ qualType expr2T
     return (tRes, EPropAssign (a, tRes) objExpr' n expr1' expr2')
inferType' env (EIndexAssign a eArr eIdx expr1 expr2) =
  do (tArr, eArr') <- inferType env eArr
     elemTVarName <- fresh
     arrTVarName <- fresh
     idxTVarName <- fresh
     let elemType = Fix . TBody . TVar $ elemTVarName
--     unify a (qualType tArr) $ Fix $ TCons TArray [elemType]
     unify a (qualType tArr) $ Fix $ TBody $ TVar arrTVarName
     (tId, eIdx') <- inferType env eIdx
     unify a (qualType tId) $ Fix $ TBody $ TVar idxTVarName
     (tExpr1, expr1') <- inferType env expr1
     unify a (qualType tExpr1) elemType
     -- TODO: BUG here, because elemTVarName never has any var instances due to the predicates usage here.
     --traceLog "EIndexAssign - applying unifyAllInstances"
     --instancePred <- unifyAllInstances a [elemTVarName]
     (tExpr2, expr2') <- inferType env expr2
     let curPred = indexAccessPred arrTVarName elemTVarName idxTVarName
     preds <- unifyPredsL a $ concat $ ([curPred]:) $ map qualPred [tArr, tId, tExpr1, tExpr2] -- TODO review
     let tRes = TQual preds $ qualType tExpr2
     return (tRes , EIndexAssign (a, tRes)  eArr' eIdx' expr1' expr2')
inferType' env (EArray a exprs) =
  do tv <- Fix . TBody . TVar <$> fresh
     te <- accumInfer env exprs
     let types = map (qualType . fst) te
     unifyl unify a $ zip (tv:types) types
     let t = qualEmpty $ Fix $ TCons TArray [tv]
     return (t, EArray (a,t) $ map snd te)
inferType' env (ETuple a exprs) =
  do te <- accumInfer env exprs
     let t = TQual (concatMap (qualPred . fst) te) $ Fix . TCons TTuple . reverse $ map (qualType . fst) te
     return (t, ETuple (a,t) $ map snd te)
inferType' env (EStringMap a exprs') =
  do let exprs = map snd exprs'
     elemType <- Fix . TBody . TVar <$> fresh
     te <- accumInfer env exprs
     let types = map (qualType . fst) te
     unifyAll a $ elemType:types
     allPreds <- unifyPredsL a . concatMap qualPred $ map fst te
     let t = TQual { qualPred = allPreds, qualType = Fix $ TCons TStringMap [elemType] }
     return (t, EStringMap (a,t) $ zip (map fst exprs') (map snd te))
inferType' env (ERow a isOpen propExprs) =
  do te <- accumInfer env $ map snd propExprs
     endVar <- RowTVar <$> fresh
     let propNamesTypes = zip propExprs (reverse $ map fst te)
         rowEnd' = TRowEnd $ if isOpen then Just endVar else Nothing
         accumRowProp' row ((propName, propExpr), propType) =
           do ts <- generalize propExpr env propType
              return $ TRowProp propName ts row
     rowType <- qualEmpty . Fix . TRow <$> foldM  accumRowProp' rowEnd' propNamesTypes
     return (rowType, ERow (a,rowType) isOpen $ zip (map fst propExprs) (map snd te))
inferType' env (ECase a eTest eBranches) =
  do (eType, eTest') <- inferType env eTest
     infPatterns <- accumInfer env $ map (ELit a . fst) eBranches
     let patternTypes = map (qualType . fst) infPatterns
     unifyAll a $ (qualType eType):patternTypes
     infBranches <- accumInfer env $ map snd eBranches
     let branchTypes = map (qualType . fst) infBranches
     unifyAll a branchTypes
     allPreds <- unifyPredsL a . concatMap qualPred $ eType : (map fst infPatterns) ++ (map fst infBranches)
     let tRes = TQual { qualPred = allPreds, qualType = qualType . fst $ head infBranches } -- TODO unsafe head
     return (tRes, ECase (a, tRes) eTest' $ zip (map fst eBranches) (map snd infBranches))
inferType' env (EProp a eObj propName) =
  do (tObj, eObj') <- inferType env eObj
     rowVar <- RowTVar <$> fresh
     propTypeScheme <- schemeEmpty . Fix . TBody . TVar <$> fresh
         --case unFix (qualType tObj) of
--                  TRow tRowList -> --TODO
--                  _ -> schemeEmpty . Fix . TBody . TVar <$> fresh
     unify a (Fix . TRow $ TRowProp propName propTypeScheme $ TRowEnd (Just rowVar)) (qualType tObj)
     propType <- instantiate propTypeScheme
     return (propType, EProp (a,propType) eObj' propName)
inferType' env (EIndex a eArr eIdx) =
  do (tArr, eArr') <- inferType env eArr
     elemTVarName <- fresh
     arrTVarName <- fresh
     idxTVarName <- fresh
     unify a (qualType tArr) (Fix $ TBody $ TVar arrTVarName)
     (tId, eIdx') <- inferType env eIdx
     unify a (qualType tId) (Fix $ TBody $ TVar idxTVarName)
     let elemType' = qualEmpty $ Fix $ TBody $ TVar elemTVarName
         curPred = indexAccessPred arrTVarName elemTVarName idxTVarName
     preds <- unifyPredsL a $ (curPred:) $ concatMap qualPred [tArr, tId] -- TODO review
     let tRes = TQual preds $ qualType elemType'
     return (tRes, EIndex (a, tRes)  eArr' eIdx')

indexAccessPred :: TVarName -> TVarName -> TVarName -> TPred Type
indexAccessPred arrTVarName elemTVarName idxTVarName =
    let --elemType = mkv elemTVarName
        mkv = Fix . TBody . TVar
    in
     TPredIsIn (ClassName "Indexable") (Fix $ TCons TTuple
                                        [ mkv arrTVarName
                                        , mkv idxTVarName
                                        , mkv elemTVarName
                                        ])
                                          -- Fix $ TCons TArray [elemType])
    -- , TPredIsIn "Index"
    --  `mkAnd` TPredEq idxTVarName (Fix $ TBody TNumber))
    -- `mkOr` (TPredEq arrTVarName (Fix $ TCons TStringMap [elemType])
    --         `mkAnd` TPredEq idxTVarName (Fix $ TBody TString))

unifyAllInstances :: Source -> [TVarName] -> Infer [TPred Type]
unifyAllInstances a tvs = do
  m <- getVarInstances
       
  traceLog $ "unifyAllInstances: " ++ pretty a ++ " Unifying all instances of tvars: " ++ intercalate ", " (map pretty tvs)
  let equivalenceSets = map Set.fromList $ filter (not . null) $ map (mapMaybe $ Graph.lab m) $ map (flip Graph.bfs m) tvs
      unifyAll' equivs =
          do  let equivsL = Set.toList equivs
                  qequivsL = map qualType equivsL
              traceLog $ "unifyAllInstances - equivalence:" ++ pretty qequivsL
              unifyAll a qequivsL
              return $ concatMap qualPred equivsL
  pred' <- concat <$> mapM unifyAll' equivalenceSets
  unifyPredsL a pred'

createEnv :: Map EVarName TypeScheme -> Infer (Map EVarName VarId)
createEnv builtins = foldM addVarScheme' Map.empty $ Map.toList builtins
    where allTVars :: TypeScheme -> Set TVarName
          allTVars (TScheme qvars t) = freeTypeVars t `Set.union` Set.fromList qvars

          addVarScheme' :: Map EVarName VarId -> (EVarName, TypeScheme) -> Infer (Map EVarName VarId)
          addVarScheme' m (name, tscheme) =
            do allocNames <- forM (Set.toList $ allTVars tscheme)
                             $ \tvName -> (tvName,) <$> fresh
               addVarScheme m name $ mapVarNames (safeLookup allocNames) tscheme


typeInference :: Map EVarName TypeScheme -> Exp Source -> Infer (Exp (Source, QualType))
typeInference builtins e =
  do env <- createEnv builtins
     (_t, e') <- inferType env e
     return e'

----------------------------------------------------------------------
--
-- | Mutable variable being assigned incompatible types:
--
-- >>> let p = emptySource
-- >>> let fun args = EAbs p ("this":args)
-- >>> let var = EVar p
-- >>> let let' = ELet p
-- >>> let tuple = ETuple p
-- >>> let lit = ELit p
-- >>> let app a b = EApp p a [lit LitUndefined, b]
-- >>> let assign = EAssign p
-- >>> let array = EArray p
--
-- x is known to have type forall a. a -> a, and to have been used in a context requiring bool -> bool (e.g. `x True`)
--
-- we now try to assign x := \y -> 2
--
-- This should fail because it "collapses" x to be Number -> Number which is not compatible with bool -> bool
--
-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))]) (assign "x" (fun ["y"] (lit (LitNumber 0))) (tuple [var "x", var "y"])))
-- ":1:1*: Error: Could not unify: Number with Boolean"
--
-- The following should succeed because x is immutable and thus polymorphic:
--
-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))]) (tuple [var "x", var "y"]))
-- "(c.(d -> d), (Number, Boolean))"
--
-- The following should fail because x is mutable and therefore a monotype:
--
-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))]) (assign "x" (fun ["z1"] (var "z1")) (tuple [var "x", var "y"])))
-- ":1:1*: Error: Could not unify: Number with Boolean"
--
-- The following should also succeed because "x" is only ever used like this: (x True). The second assignment to x is: x := \z1 -> False, which is specific but matches the usage. Note that x's type is collapsed to: Boolean -> Boolean.
--
-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (app (var "x") (lit (LitBoolean True))) (assign "x" (fun ["z1"] (lit (LitBoolean False))) (tuple [var "x", var "y"])))
-- "((Boolean -> Boolean), Boolean)"
--
-- | Tests a setter for x being called with something more specific than x's original definition:
-- >>> :{
-- >>> test $ let'
-- >>> "x" (fun ["a"] (var "a"))
-- >>> (let' "setX"
-- >>>    (fun ["v"]
-- >>>             (let'
-- >>>          "_" (assign "x" (var "v") (var "x")) (lit (LitBoolean False))))
-- >>>    (let'
-- >>>       "_" (app (var "setX") (fun ["a"] (lit (LitString "a"))))
-- >>>       (app (var "x") (lit (LitBoolean True)))))
-- >>> :}
-- ":1:1*: Error: Could not unify: String with Boolean"
--
-- >>> test $ tuple [lit (LitBoolean True), lit (LitNumber 2)]
-- "(Boolean, Number)"
--
-- >>> test $ let' "id" (fun ["x"] (var "x")) (assign "id" (fun ["y"] (var "y")) (var "id"))
-- "a.(b -> b)"
--
-- >>> test $ let' "id" (fun ["x"] (var "x")) (assign "id" (lit (LitBoolean True)) (var "id"))
-- ":1:1*: Error: Could not unify: a.(b -> b) with Boolean"
--
-- >>> test $ let' "x" (lit (LitBoolean True)) (assign "x" (lit (LitBoolean False)) (var "x"))
-- "Boolean"
--
-- >>> test $ let' "x" (lit (LitBoolean True)) (assign "x" (lit (LitNumber 3)) (var "x"))
-- ":1:1*: Error: Could not unify: Boolean with Number"
--
-- >>> test $ let' "x" (array [lit (LitBoolean True)]) (var "x")
-- "[Boolean]"
--
-- >>> test $ let' "x" (array [lit $ LitBoolean True, lit $ LitBoolean False]) (var "x")
-- "[Boolean]"
--
-- >>> test $ let' "x" (array []) (assign "x" (array []) (var "x"))
-- "[a]"
--
-- >>> test $ let' "x" (array [lit $ LitBoolean True, lit $ LitNumber 2]) (var "x")
-- ":1:1*: Error: Could not unify: Number with Boolean"
--
-- >>> test $ let' "id" (fun ["x"] (let' "y" (var "x") (var "y"))) (app (var "id") (var "id"))
-- "c.(d -> d)"
--
-- >>> test $ let' "id" (fun ["x"] (let' "y" (var "x") (var "y"))) (app (app (var "id") (var "id")) (lit (LitNumber 2)))
-- "Number"
--
-- >>> test $ let' "id" (fun ["x"] (app (var "x") (var "x"))) (var "id")
-- ":1:1*: Error: Occurs check failed: a in (a -> b)"
--
-- >>> test $ fun ["m"] (let' "y" (var "m") (let' "x" (app (var "y") (lit (LitBoolean True))) (var "x")))
-- "a.((Boolean -> b) -> b)"
--
-- >>> test $ app (lit (LitNumber 2)) (lit (LitNumber 2))
-- ":1:1*: Error: Could not unify: Number with (Number -> a)"
--
-- EAssign tests
-- >>> test $ let' "x" (fun ["y"] (lit (LitNumber 0))) (assign "x" (fun ["y"] (var "y")) (var "x"))
-- "a.(Number -> Number)"
--
-- >>> test $ let' "x" (fun ["y"] (var "y")) (assign "x" (fun ["y"] (lit (LitNumber 0))) (var "x"))
-- "a.(Number -> Number)"
--
-- >>> test $ let' "x" (fun ["y"] (var "y")) (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))])
-- "(Number, Boolean)"
--
-- >>> test $ let' "x" (fun ["y"] (var "y")) (app (var "x") (var "x"))
-- "c.(d -> d)"
--
-- >>> test $ let' "x" (fun ["a"] (var "a")) (let' "getX" (fun ["v"] (var "x")) (let' "setX" (fun ["v"] (let' "_" (assign "x" (var "v") (var "x")) (lit (LitBoolean True)))) (let' "_" (app (var "setX") (fun ["a"] (lit (LitString "a")))) (var "getX"))))
-- "e.(f -> d.(String -> String))"
test :: Exp Source -> String
test e = case runTypeInference e of
          Left err -> pretty err
          Right expr -> pretty $ snd . head . getAnnotations . minifyVars $ expr


runTypeInference :: Exp Source -> Either TypeError (Exp (Source, QualType))
runTypeInference e = runInfer $ typeInference Operators.builtins e