[ re agda#357 ] Check that we do not compile Level or Size

src/Agda2Hs/Compile/Type.hs

@@ -22,14 +22,14 @@ import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
 import Agda.TypeChecking.Pretty
-import Agda.TypeChecking.Reduce ( reduce, unfoldDefinitionStep )
+import Agda.TypeChecking.Reduce ( reduce, unfoldDefinitionStep, instantiate )
 import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope
 
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda.Utils.List ( downFrom )
 import Agda.Utils.Maybe ( ifJustM, fromMaybe )
-import Agda.Utils.Monad ( ifM, unlessM, and2M, or2M )
+import Agda.Utils.Monad ( ifM, whenM, unlessM, and2M, or2M )
 import Agda.Utils.Size ( Sized(size) )
 import Agda.Utils.Functor ( ($>) )
 
@@ -89,7 +89,9 @@ compileType t = do
   reportSDoc "agda2hs.compile.type" 12 $ text "Compiling type" <+> prettyTCM t
   reportSDoc "agda2hs.compile.type" 22 $ text "Compiling type" <+> pretty t
 
-  case t of
+  whenM (isErasedBaseType t) fail
+
+  instantiate t >>= \case
     Pi a b -> do
       let compileB = underAbstraction a b (compileType . unEl)
       compileDomType (absName b) a >>= \case

src/Agda2Hs/Compile/Utils.hs

@@ -141,11 +141,17 @@ canErase :: Type -> C Bool
 canErase a = do
   TelV tel b <- telView a
   addContext tel $ orM
-    [ isLevelType b                       -- Level
-    , isJust <$> isSizeType b             -- Size
-    , isPropSort (getSort b)              -- _ : Prop
+    [ isErasedBaseType (unEl b)
+    , isPropSort (getSort b)            -- _ : Prop
     ]
 
+isErasedBaseType :: Term -> C Bool
+isErasedBaseType x = orM
+  [ isLevelType b                       -- Level
+  , isJust <$> isSizeType b             -- Size
+  ]
+  where b = El __DUMMY_SORT__ x
+
 -- Exploits the fact that the name of the record type and the name of the record module are the
 -- same, including the unique name ids.
 isClassFunction :: QName -> C Bool