+lookup :: String -> Typing Scheme
+lookup k = gamma >>= \g-> case 'Map'.member k g of
+ False = liftT (Left $ UndeclaredVariableError zero k)
+ True = pure ('Map'.find k g)
+
+//The inference class
+//When tying it all together we will treat the program is a big
+//let x=e1 in let y=e2 in ....
+class infer a :: a -> Typing (Substitution, Type)
+
+instance infer Expr where
+ infer e = case e of
+ VarExpr _ (VarDef k fs) = (\t->(zero,t)) <$> (lookup k >>= instantiate)
+ //instantiate is key for the let polymorphism!
+
+ Op2Expr _ e1 op e2 =
+ infer e1 >>= \(s1, t1) ->
+ infer e2 >>= \(s2, t2) ->
+ fresh >>= \tv ->
+ let given = t1 ->> t2 ->> tv in
+ op2Type op >>= \expected ->
+ lift (unify expected given) >>= \s3 ->
+ pure ((compose s1 $ compose s2 s3), subst s3 tv)
+
+ Op1Expr _ op e1 =
+ infer e1 >>= \(s1, t1) ->
+ fresh >>= \tv ->
+ let given = t1 ->> tv in
+ op1Type op >>= \expected ->
+ lift (unify expected given) >>= \s2 ->
+ pure ((compose s1 s2), subst s2 tv)
+
+
+
+ IntExpr _ _ = pure $ (zero, IntType)
+ BoolExpr _ _ = pure $ (zero, BoolType)
+ CharExpr _ _ = pure $ (zero, CharType)
+
+
+op2Type :: Op2 -> Typing Type
+op2Type op
+| elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
+ = pure (IntType ->> IntType ->> IntType)
+| elem op [BiEquals, BiUnEqual]
+ = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
+| elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
+ = pure (IntType ->> IntType ->> BoolType)
+| elem op [BiAnd, BiOr]
+ = pure (BoolType ->> BoolType ->> BoolType)
+| op == BiCons
+ = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)
+
+op1Type :: Op1 -> Typing Type
+op1Type UnNegation = pure $ (BoolType ->> BoolType)
+op1Type UnMinus = pure $ (IntType ->> IntType)