Properly handle unreachable clauses (#30)

* add empty type matching, remove let for case default
* put empty type at the beginning of the environment

Author: flupe

src/Agda/Utils/EliminateDefaults.hs

@@ -4,11 +4,6 @@ Taken straight from Agda source.
 There are two important differences:
 - we also add branches for unreachable defaults (because we need all cases to be exhaustive)
 - we sort the case alts according to the order of constructors for the given inductive
-
-Currently, the default branch value is bound in a let binding,
-I don't know if this will be problematic for some targets that evaluate
-the binding before the case. Will they fail?
-
 -}
 
 -- | Eliminates case defaults by adding an alternative for all possible
@@ -22,7 +17,7 @@ import Control.Monad.IO.Class (liftIO)
 import Agda.Syntax.Treeless
 import Agda.TypeChecking.Monad
 import Agda.TypeChecking.Substitute
-import Agda.Compiler.Treeless.Subst () --instance only
+import Agda.Compiler.Treeless.Subst () -- instance only
 
 
 eliminateCaseDefaults :: TTerm -> TCM TTerm
@@ -35,35 +30,30 @@ eliminateCaseDefaults = tr
 
         let missingCons = dtCons List.\\ map aCon alts
         def <- tr def
-        newAlts <- forM missingCons $ \con -> do
+
+        -- we produce a new alternative for every missing constructor
+        -- whose body is the default body, raised by #args brought in scope
+        newAlts <- forM missingCons \con -> do
           Constructor {conArity = ar} <- theDef <$> getConstInfo con
-          return $ TACon con ar (TVar ar)
+          return $ TACon con ar $ raise ar def
 
-        alts' <- (++ newAlts) <$> mapM (trAlt . raise 1) alts
+        alts' <- (++ newAlts) <$> mapM trAlt alts
 
-        -- sort the alts
-        let alts'' = flip List.sortOn alts' \alt -> List.elemIndex (aCon alt) dtCons 
+        -- then we sort the alts
+        let alts'' = flip List.sortOn alts' \alt -> List.elemIndex (aCon alt) dtCons
 
-        return $ TLet def $ TCase (sc + 1) ct tUnreachable alts''
+        return $ TCase sc ct tUnreachable alts''
 
       -- case on non-data are always exhaustive
       TCase sc ct def alts -> TCase sc ct <$> tr def <*> mapM trAlt alts
 
-      t@TVar{}    -> return t
-      t@TDef{}    -> return t
-      t@TCon{}    -> return t
-      t@TPrim{}   -> return t
-      t@TLit{}    -> return t
-      t@TUnit{}   -> return t
-      t@TSort{}   -> return t
-      t@TErased{} -> return t
-      t@TError{}  -> return t
-
       TCoerce a -> TCoerce <$> tr a
       TLam b    -> TLam <$> tr b
       TApp a bs -> TApp <$> tr a <*> mapM tr bs
       TLet e b  -> TLet <$> tr e <*> tr b
 
+      t -> return t
+
     trAlt :: TAlt -> TCM TAlt
     trAlt = \case
       TAGuard g b -> TAGuard <$> tr g <*> tr b

src/Agda2Lambox/Compile.hs

@@ -28,6 +28,7 @@ import Agda2Lambox.Compile.Inductive  ( compileInductive )
 import Agda2Lambox.Compile.TypeScheme ( compileTypeScheme )
 import Agda2Lambox.Compile.Type       ( compileTopLevelType )
 
+import LambdaBox ( emptyName, emptyDecl )
 import LambdaBox.Names
 import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), ConstantBody(..))
 import LambdaBox.Term (Term(LBox))
@@ -38,7 +39,7 @@ import LambdaBox.Term (Term(LBox))
 compile :: Target t -> [QName] -> CompileM (GlobalEnv t)
 compile t qs = do
   items <- compileLoop (compileDefinition t) qs
-  pure $ GlobalEnv $ map itemToEntry items
+  pure $ GlobalEnv $ map itemToEntry items ++ [(emptyName, emptyDecl t)]
   where
     itemToEntry :: CompiledItem (GlobalDecl t) -> (KerName, GlobalDecl t)
     itemToEntry CompiledItem{..} = (qnameToKName itemName, itemValue)

src/Agda2Lambox/Compile/Term.hs

@@ -26,7 +26,7 @@ import Agda.TypeChecking.Monad.Base ( TCM , liftTCM, MonadTCEnv, MonadTCM )
 import Agda.TypeChecking.Monad.Builtin ( getBuiltinName_ )
 
 import LambdaBox.Names ( Name(..) )
-import LambdaBox ( Term(..) )
+import LambdaBox ( Term(..), emptyName )
 import LambdaBox qualified as LBox
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
@@ -144,7 +144,11 @@ compileTermC = \case
   TSort   -> return LBox
   TErased -> return LBox
 
-  TError terr -> return LBox -- unreachable clause
+  TError terr -> return $ LCase (LBox.Inductive emptyName 0) 0 LBox []
+    -- ^ Unreachable clause.
+    --   We explicitely match on the empty type (for which we do not construct a proof),
+    --   so that later passes recognize that this is unreachable.
+
   TCoerce tt  -> genericError "Coerces not supported."
 
 compileLit :: Literal -> C LBox.Term

src/LambdaBox.hs

@@ -5,9 +5,35 @@ module LambdaBox
   , module LambdaBox.Term
   , module LambdaBox.Type
   , module LambdaBox.Env
+  , emptyName
+  , emptyDecl
   ) where
 
+import Control.Monad.Identity
+import Agda2Lambox.Compile.Target
 import LambdaBox.Names
 import LambdaBox.Term
 import LambdaBox.Type
 import LambdaBox.Env
+
+-- | Kername for the backed-in empty type.
+emptyName :: KerName
+emptyName = KerName (MPFile ["LamBox"]) "Empty"
+
+-- | Backed-in definition for the empty type.
+--   Used to discard unreachable branches in typed targets.
+emptyDecl :: Target t -> GlobalDecl t
+emptyDecl t = InductiveDecl MutualInductive
+  { indFinite = Finite
+  , indPars   = 0
+  , indBodies = [
+      OneInductive
+        { indName          = "Empty"
+        , indPropositional = False
+        , indKElim         = IntoAny
+        , indTypeVars      = runIdentity $ whenTyped t $ pure []
+        , indCtors         = []
+        , indProjs         = []
+        }
+    ]
+  }