Improved type inference

src/tests/encore/basic/BottomError.enc

@@ -0,0 +1,11 @@
+active class Main
+  def main() : unit
+    this.test5()
+  end
+
+  def test5() : int
+    val dummy = return 5
+    println("{}", dummy.l)
+    30
+  end
+end

src/tests/encore/basic/BottomError.fail

@@ -0,0 +1 @@
+Cannot read field of expression 'dummy' of bottom type Bottom

src/tests/encore/basic/ifNothing.enc

@@ -7,5 +7,6 @@ active class Main
     else
       Nothing
     end
+    println("Done")
   end
 end

src/tests/encore/basic/ifNothing.out

@@ -0,0 +1 @@
+Done

src/tests/encore/match/nothing.enc

@@ -2,7 +2,7 @@ active class Main
   def main(args : [String]) : unit
     match Nothing with
       case Nothing =>
-        println("Until the typechecker gets clever enough, this won't compile")
+        println("This now compiles.")
       end
     end
   end

src/tests/encore/match/nothing.out

@@ -0,0 +1 @@
+This now compiles.

src/tests/encore/regressions/784.enc

@@ -0,0 +1,30 @@
+active class Base
+  def base() : int
+    42
+  end
+end
+
+active class Bar
+  def bar() : int
+    24
+  end
+end
+
+active class Foo
+  def foo(b : bool) : int
+    val arg1 = (new Bar) ! bar()
+    val arg2 = (new Base) ! base()
+    forward(if b then
+              forward(arg1)
+            else
+              arg2
+            end)
+  end
+end
+
+active class Main
+  def main() : unit
+    println("{}", get((new Foo) ! foo(true)))
+    println("{}", get((new Foo) ! foo(false)))
+  end
+end

src/tests/encore/regressions/784.out

@@ -0,0 +1,2 @@
+24
+42

src/tests/encore/regressions/836.enc

@@ -1,5 +1,55 @@
 active class Main
   def main() : unit
-    println("{}", Nothing)
+    this.test1()
+    println("{}", this.test2())
+    this.test3()
+    println("{}", this.test4())
+    println("{}", this.test5())
+    println("{}", this.test6())
+  end
+
+  def test1() : unit
+     println("{}", Nothing)
+  end
+
+  def test2() : int
+    match Nothing with
+      case Nothing => 0
+      case Just(ice) => 1
+    end
+  end
+
+  def test3() : unit
+    match Nothing with
+      case Nothing =>
+        println("Nothing")
+      end
+    end
+  end
+
+  def test4() : int
+    match Nothing with
+      case Just(ice) => ice
+      case _ => 0
+    end
+  end
+
+  def test5() : int
+    val dummy = return 5
+    30
+  end
+
+
+  def test6() : int
+    val dummy = return 5
+    val d : C = dummy
+    d.foo()
+  end
+
+end
+
+local class C
+  def foo() : int
+    100
   end
 end

src/tests/encore/regressions/836.out

@@ -1 +1,6 @@
 Nothing
+0
+Nothing
+0
+5
+5

src/types/Typechecker/Typechecker.hs

@@ -928,8 +928,6 @@ instance Checkable Expr where
                                    in map (extractBindings ty) vars
                locals = concatMap extract eDecls
                declTypes = map snd locals
-           when (any isBottomType (concatMap typeComponents declTypes)) $
-                tcError BottomTypeInferenceError
            let addNames = (if mutability == Val
                            then extendEnvironmentImmutable
                            else extendEnvironment) locals
@@ -1055,8 +1053,6 @@ instance Checkable Expr where
           when (isActiveSingleType argType) $
             unless (isThisAccess arg) $
               tcError ActiveMatchError
-          when (any isBottomType (typeComponents argType)) $
-               pushError arg BottomTypeInferenceError
           when (any isNullType (typeComponents argType)) $
                pushError arg NullTypeInferenceError
 
@@ -1283,7 +1279,7 @@ instance Checkable Expr where
 
     --  E |- val : Fut t
     -- ------------------
-    --  E |- forward val : t
+    --  E |- forward val : _|_
     doTypecheck forward@(Forward {forwardExpr}) =
         do eExpr <- typecheck forwardExpr
            let ty = AST.getType eExpr
@@ -1296,7 +1292,7 @@ instance Checkable Expr where
                let returnType = methodType mdecl
                unlessM (getResultType ty `subtypeOf` returnType) $
                        pushError eExpr $ ForwardTypeError returnType ty
-               return $ setType (getResultType ty) forward {forwardExpr = eExpr}
+               return $ setType bottomType forward {forwardExpr = eExpr}
              _ -> pushError eExpr ForwardInFunction
 
     --  E |- val : t

src/types/Typechecker/Util.hs

@@ -54,7 +54,6 @@ import AST.AST as AST
 import Data.List
 import Data.Maybe
 import Text.Printf (printf)
-import Debug.Trace
 import Control.Monad.Reader
 import Control.Monad.Except
 import Control.Arrow(second)
@@ -379,7 +378,7 @@ subtypeOf sub super
     | isUnionType super = do
         let members2 = unionMembers super
         anyM (sub `subtypeOf`) members2
-    | isBottomType sub && (not . isBottomType $ super) = return True
+    | isBottomType sub = return True
     | isNumeric sub && isNumeric super =
         return $ sub `numericSubtypeOf` super
     | isTypeVar sub && not (isTypeVar super)
@@ -654,6 +653,8 @@ doUnifyTypes inter args@(ty:tys)
         doUnifyTypes inter tys
     | isBottomType ty =
         doUnifyTypes inter tys
+    | isBottomType inter =
+        doUnifyTypes ty tys
     | isClassType ty =
         if ty == inter
         then doUnifyTypes inter tys

src/types/Types.hs

@@ -527,7 +527,7 @@ hasSameKind ty1 ty2
     areBoth isParType ||
     areBoth isArrayType ||
     areBoth isStreamType = getResultType ty1 `hasSameKind` getResultType ty2
-  | (isBottomTy1 || isBottomTy2) && not (areBoth isBottomType) = True -- xor
+  | (isBottomTy1 || isBottomTy2) = True
   | areBoth isPrimitive ||
     areBoth isTupleType ||
     areBoth isTypeVar ||