[ Issue 1428 ] New sort SizeUniv, but unused yet.

SizeUniv will be the sort of builtin types SIZE and SIZELT.
Its purpose is to prevent building functions on Size, especially
(pred : (i : Size) -> Size< i) which triggers issue 1428.

So far, it is unused, as a new Sort is incompatible with the
current (hackish) handling of sort metas, which assumes that every sort
is of the form Set x for some level x (including infinity to represent
sort Inf).  To activate SizeUniv, we need proper sort metas first.

src/full/Agda/Syntax/Internal.hs

@@ -203,6 +203,7 @@ data Sort
   = Type Level  -- ^ @Set ℓ@.
   | Prop        -- ^ Dummy sort.
   | Inf         -- ^ @Setω@.
+  | SizeUniv    -- ^ @SizeUniv@, a sort inhabited by type @Size@.
   | DLub Sort (Abs Sort)
     -- ^ Dependent least upper bound.
     --   If the free variable occurs in the second sort,
@@ -623,6 +624,7 @@ varSort n = Type $ Max [Plus 0 $ NeutralLevel mempty $ Var n []]
 sSuc :: Sort -> Sort
 sSuc Prop            = mkType 1
 sSuc Inf             = Inf
+sSuc SizeUniv        = SizeUniv
 sSuc (DLub a b)      = DLub (sSuc a) (fmap sSuc b)
 sSuc (Type l)        = Type $ levelSuc l
 
@@ -933,6 +935,7 @@ instance KillRange Sort where
   killRange s = case s of
     Prop       -> Prop
     Inf        -> Inf
+    SizeUniv   -> SizeUniv
     Type a     -> killRange1 Type a
     DLub s1 s2 -> killRange2 DLub s1 s2
 
@@ -1050,6 +1053,7 @@ instance Pretty Sort where
       Type l -> mparens (p > 9) $ text "Set" <+> prettyPrec 10 l
       Prop -> text "Prop"
       Inf -> text "Setω"
+      SizeUniv -> text "SizeUniv"
       DLub s b -> mparens (p > 9) $
         text "dlub" <+> prettyPrec 10 s
                     <+> parens (sep [ text ("λ " ++ show (absName b) ++ " ->")

src/full/Agda/Syntax/Internal/Defs.hs

@@ -82,6 +82,7 @@ instance GetDefs Sort where
     Type l    -> getDefs l
     Prop      -> return ()
     Inf       -> return ()
+    SizeUniv  -> return ()
     DLub s s' -> getDefs s >> getDefs s'
 
 instance GetDefs Level where

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

@@ -51,6 +51,7 @@ import Agda.Syntax.Internal as I
 import qualified Agda.Utils.VarSet as VSet
 
 import Agda.TypeChecking.Monad as M hiding (MetaInfo)
+import Agda.TypeChecking.Monad.Builtin
 import Agda.TypeChecking.Reduce
 import {-# SOURCE #-} Agda.TypeChecking.Records
 import Agda.TypeChecking.CompiledClause (CompiledClauses(Fail))
@@ -903,6 +904,9 @@ instance Reify Sort Expr where
           return $ A.App exprInfo (A.Set exprInfo 0) (defaultNamedArg a)
         I.Prop       -> return $ A.Prop exprInfo
         I.Inf       -> A.Var <$> freshName_ ("Setω" :: String)
+        I.SizeUniv  -> do
+          I.Def sizeU [] <- primSizeUniv
+          return $ A.Def sizeU
         I.DLub s1 s2 -> do
           lub <- freshName_ ("dLub" :: String) -- TODO: hack
           (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)

src/full/Agda/Termination/TermCheck.hs

@@ -712,6 +712,7 @@ instance ExtractCalls Sort where
     case s of
       Prop       -> return empty
       Inf        -> return empty
+      SizeUniv   -> return empty
       Type t     -> terUnguarded $ extract t  -- no guarded levels
       DLub s1 s2 -> extract (s1, s2)
 

src/full/Agda/TypeChecking/Abstract.hs

@@ -87,6 +87,7 @@ instance AbstractTerm Sort where
     Type n     -> Type $ absS n
     Prop       -> Prop
     Inf        -> Inf
+    SizeUniv   -> SizeUniv
     DLub s1 s2 -> DLub (absS s1) (absS s2)
     where absS x = abstractTerm u x
 

src/full/Agda/TypeChecking/CheckInternal.hs

@@ -128,6 +128,7 @@ checkInternal v t = do
         checkInternal (absBody vb) (absBody b)
     Pi a b     -> do
       s <- shouldBeSort t
+      when (s == SizeUniv) $ typeError $ FunctionTypeInSizeUniv v
       let st = sort s
       checkInternal (unEl $ unDom a) st
       addContext (absName b, a) $ do
@@ -304,6 +305,7 @@ checkSort s =
       -- the dummy Prop should not be part of a term we check
     Inf      -> typeError $ SetOmegaNotValidType
       -- we cannot have Setω on the lhs of the colon
+    SizeUniv -> typeError $ InvalidTypeSort s
     DLub a b -> do
       checkSort a
       addContext (absName b, defaultDom (sort a) :: I.Dom Type) $ do

src/full/Agda/TypeChecking/Conversion.hs

@@ -967,6 +967,10 @@ compareSort CmpEq  = equalSort
 compareSort CmpLeq = leqSort
 
 -- | Check that the first sort is less or equal to the second.
+--
+--   We can put @SizeUniv@ below @Inf@, but otherwise, it is
+--   unrelated to the other universes.
+--
 leqSort :: Sort -> Sort -> TCM ()
 leqSort s1 s2 = catchConstraint (SortCmp CmpLeq s1 s2) $ do
   (s1,s2) <- reduce (s1,s2)
@@ -988,6 +992,9 @@ leqSort s1 s2 = catchConstraint (SortCmp CmpLeq s1 s2) $ do
       (Prop    , Type _  ) -> yes
       (Type _  , Prop    ) -> no
 
+      (SizeUniv, SizeUniv) -> yes
+      (SizeUniv, _       ) -> no
+      (_       , SizeUniv) -> no
 
       (Inf     , _       ) -> unlessM typeInType $ equalSort s1 s2
       (DLub{}  , _       ) -> unlessM typeInType $ postpone
@@ -1298,6 +1305,9 @@ equalSort s1 s2 = do
 
             (Type a  , Type b  ) -> equalLevel a b
 
+            (SizeUniv, SizeUniv) -> yes
+            (SizeUniv, _       ) -> no
+            (_       , SizeUniv) -> no
 
             (Prop    , Prop    ) -> yes
             (Type _  , Prop    ) -> no

src/full/Agda/TypeChecking/Errors.hs

@@ -190,6 +190,8 @@ errorString err = case err of
   NotAProperTerm                           -> "NotAProperTerm"
   SetOmegaNotValidType{}                   -> "SetOmegaNotValidType"
   InvalidType{}                            -> "InvalidType"
+  InvalidTypeSort{}                        -> "InvalidTypeSort"
+  FunctionTypeInSizeUniv{}                 -> "FunctionTypeInSizeUniv"
   NotAValidLetBinding{}                    -> "NotAValidLetBinding"
   NotAnExpression{}                        -> "NotAnExpression"
   NotImplemented{}                         -> "NotImplemented"
@@ -487,8 +489,13 @@ instance PrettyTCM TypeError where
 
     SetOmegaNotValidType -> fwords "Setω is not a valid type"
 
+    InvalidTypeSort s -> fsep $ [prettyTCM s] ++ pwords "is not a valid type"
     InvalidType v -> fsep $ [prettyTCM v] ++ pwords "is not a valid type"
 
+    FunctionTypeInSizeUniv v -> fsep $
+      pwords "Functions may not return sizes, thus, function type " ++
+      [ prettyTCM v ] ++ pwords " is illegal"
+
     SplitOnIrrelevant p t -> fsep $
       pwords "Cannot pattern match" ++ [prettyA p] ++
       pwords "against irrelevant type" ++ [prettyTCM t]

src/full/Agda/TypeChecking/Free.hs

@@ -280,6 +280,7 @@ instance Free Sort where
       Type a     -> freeVars' a
       Prop       -> mempty
       Inf        -> mempty
+      SizeUniv   -> mempty
       DLub s1 s2 -> weakly <$> freeVars' (s1, s2)
 
 instance Free Level where

src/full/Agda/TypeChecking/MetaVars/Mention.hs

@@ -53,6 +53,7 @@ instance MentionsMeta Sort where
     Type l     -> mentionsMeta x l
     Prop       -> False
     Inf        -> False
+    SizeUniv   -> False
     DLub s1 s2 -> mentionsMeta x (s1, s2)
 
 instance MentionsMeta t => MentionsMeta (Abs t) where

src/full/Agda/TypeChecking/MetaVars/Occurs.hs

@@ -404,6 +404,7 @@ instance Occurs Sort where
       Type a     -> Type <$> occurs red ctx m xs a
       Prop       -> return s'
       Inf        -> return s'
+      SizeUniv   -> return s'
 
   metaOccurs m s = do
     s <- instantiate s
@@ -412,6 +413,7 @@ instance Occurs Sort where
       Type a     -> metaOccurs m a
       Prop       -> return ()
       Inf        -> return ()
+      SizeUniv   -> return ()
 
 instance Occurs a => Occurs (Elim' a) where
   occurs red ctx m xs e@Proj{}  = return e
@@ -602,6 +604,7 @@ instance FoldRigid Sort where
       Type l     -> fold l
       Prop       -> mempty
       Inf        -> mempty
+      SizeUniv   -> mempty
       DLub s1 s2 -> fold (s1, s2)
     where fold = foldRigid abs f
 

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -1825,8 +1825,13 @@ data TypeError
         | NotAProjectionPattern (A.NamedArg A.Pattern)
         | NotAProperTerm
         | SetOmegaNotValidType
+        | InvalidTypeSort Sort
+            -- ^ This sort is not a type expression.
         | InvalidType Term
             -- ^ This term is not a type expression.
+        | FunctionTypeInSizeUniv Term
+            -- ^ This term, a function type constructor, lives in
+            --   @SizeUniv@, which is not allowed.
         | SplitOnIrrelevant A.Pattern (Dom Type)
         | DefinitionIsIrrelevant QName
         | VariableIsIrrelevant Name

src/full/Agda/TypeChecking/Primitive.hs

@@ -527,6 +527,12 @@ el t = El (mkType 0) <$> t
 tset :: TCM Type
 tset = return $ sort (mkType 0)
 
+tSetOmega :: TCM Type
+tSetOmega = return $ sort Inf
+
+tSizeUniv :: TCM Type
+tSizeUniv = return $ sort SizeUniv
+
 -- | Abbreviation: @argN = 'Arg' 'defaultArgInfo'@.
 argN :: e -> I.Arg e
 argN = Arg defaultArgInfo

src/full/Agda/TypeChecking/Quote.hs

@@ -139,6 +139,7 @@ quotingKit = do
       quoteSort (Type t) = quoteSortLevelTerm t
       quoteSort Prop     = pure unsupportedSort
       quoteSort Inf      = pure unsupportedSort
+      quoteSort SizeUniv = pure unsupportedSort
       quoteSort DLub{}   = pure unsupportedSort
 
       quoteType :: Type -> ReduceM Term

src/full/Agda/TypeChecking/Reduce.hs

@@ -233,6 +233,7 @@ instance Reduce Sort where
             Prop       -> return s
             Type s'    -> levelSort <$> reduce' s'
             Inf        -> return Inf
+            SizeUniv   -> return SizeUniv
 
 instance Reduce Elim where
   reduce' (Apply v) = Apply <$> reduce' v
@@ -649,6 +650,7 @@ instance Simplify Sort where
         Type s     -> levelSort <$> simplify' s
         Prop       -> return s
         Inf        -> return s
+        SizeUniv   -> return s
 
 instance Simplify Level where
   simplify' (Max as) = levelMax <$> simplify' as
@@ -758,6 +760,7 @@ instance Normalise Sort where
         Prop       -> return s
         Type s     -> levelSort <$> normalise' s
         Inf        -> return Inf
+        SizeUniv   -> return SizeUniv
 
 instance Normalise Type where
     normalise' (El s t) = El <$> normalise' s <*> normalise' t
@@ -899,6 +902,7 @@ instance InstantiateFull Sort where
             Prop       -> return s
             DLub s1 s2 -> dLub <$> instantiateFull' s1 <*> instantiateFull' s2
             Inf        -> return s
+            SizeUniv   -> return s
 
 instance InstantiateFull Type where
     instantiateFull' (El s t) =

src/full/Agda/TypeChecking/Rules/Term.hs

@@ -735,12 +735,22 @@ checkExpr e t0 =
                    , nest 2 $ text "t   =" <+> prettyTCM t'
                    , nest 2 $ text "cxt =" <+> (prettyTCM =<< getContextTelescope)
                    ]
+            when (s == SizeUniv) $ do
+              -- Andreas, 2015-02-14
+              -- We have constructed a function type in SizeUniv
+              -- which is illegal to prevent issue 1428.
+              typeError $ FunctionTypeInSizeUniv v
             coerce v (sort s) t
         A.Fun _ (Arg info a) b -> do
             a' <- isType_ a
             b' <- isType_ b
             s <- reduce $ getSort a' `sLub` getSort b'
             let v = Pi (convColor $ Dom info a') (NoAbs underscore b')
+            when (s == SizeUniv) $ do
+              -- Andreas, 2015-02-14
+              -- We have constructed a function type in SizeUniv
+              -- which is illegal to prevent issue 1428.
+              typeError $ FunctionTypeInSizeUniv v
             coerce v (sort s) t
         A.Set _ n    -> do
           n <- ifM typeInType (return 0) (return n)

src/full/Agda/TypeChecking/Serialise.hs

@@ -986,10 +986,12 @@ instance EmbPrj LevelAtom where
 instance EmbPrj I.Sort where
   icod_ (Type  a  ) = icode1' a
   icod_ Prop        = icode1 1 ()
+  icod_ SizeUniv    = icode1 3 ()
   icod_ Inf         = icode1 4 ()
   icod_ (DLub a b)  = __IMPOSSIBLE__
   value = vcase valu where valu [a]    = valu1 Type  a
                            valu [1, _] = valu0 Prop
+                           valu [3, _] = valu0 SizeUniv
                            valu [4, _] = valu0 Inf
                            valu _      = malformed
 

src/full/Agda/TypeChecking/Substitute.hs

@@ -663,6 +663,7 @@ instance Subst Sort where
     Type n     -> levelSort $ sub n
     Prop       -> Prop
     Inf        -> Inf
+    SizeUniv   -> SizeUniv
     DLub s1 s2 -> DLub (sub s1) (sub s2)
     where sub x = applySubst rho x
 
@@ -1097,6 +1098,8 @@ sLub s Prop = s
 sLub Prop s = s
 sLub Inf _ = Inf
 sLub _ Inf = Inf
+sLub SizeUniv s = s         -- one can freely quantify over sizes in any Set
+sLub _ SizeUniv = SizeUniv  -- but everything resulting in a size lives in the SizeUniv
 sLub (Type (Max as)) (Type (Max bs)) = Type $ levelMax (as ++ bs)
 sLub (DLub a b) c = DLub (sLub a c) b
 sLub a (DLub b c) = DLub (sLub a b) c

src/full/Agda/TypeChecking/Test/Generators.hs

@@ -449,6 +449,7 @@ instance ShrinkC Sort Sort where
     Type n     -> [] -- No Level instance yet -- Type <$> shrinkC conf n
     Prop       -> __IMPOSSIBLE__
     Inf        -> []
+    SizeUniv   -> []
     DLub s1 s2 -> __IMPOSSIBLE__
   noShrink = id