Unfixing #1428. SizeUniv deactivated.

With SizeUniv, sorts are no longer linear order, and the ptsRule is no
longer just maximum (lub).  This could be implemented properly, but is
serious effort due to the optimizations done for levels.

This patch defines SizeUniv = Set, so all the code for SizeUniv should
be dead.  I keep it, because I might come back and implement the ptsRule
properly.

src/full/Agda/TypeChecking/Primitive.hs

@@ -537,8 +537,15 @@ tset = return $ sort (mkType 0)
 tSetOmega :: TCM Type
 tSetOmega = return $ sort Inf
 
+sSizeUniv :: Sort
+sSizeUniv = mkType 0
+-- Andreas, 2016-04-14 switching off SizeUniv, unfixing issue #1428
+-- sSizeUniv = SizeUniv
+
 tSizeUniv :: TCM Type
-tSizeUniv = return $ El SizeUniv $ Sort SizeUniv
+tSizeUniv = tset
+-- Andreas, 2016-04-14 switching off SizeUniv, unfixing issue #1428
+-- tSizeUniv = return $ El sSizeUniv $ Sort sSizeUniv
 -- Andreas, 2015-03-16 Since equality checking for types
 -- includes equality checking for sorts, we cannot put
 -- SizeUniv in Setω.  (SizeUniv : Setω) == (_0 : suc _0)

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

@@ -192,7 +192,7 @@ coreBuiltins = map (\ (x, z) -> BuiltinInfo x z)
         tchar      = el primChar
         tstring    = el primString
         tqname     = el primQName
-        tsize      = El SizeUniv <$> primSize
+        tsize      = El sSizeUniv <$> primSize
         tbool      = el primBool
         thiding    = el primHiding
         trelevance = el primRelevance
@@ -487,7 +487,7 @@ bindBuiltinNoDef b q = do
         -- Andreas, 2015-02-14
         -- Special treatment of SizeUniv, should maybe be a primitive.
         def | b == builtinSizeUniv = emptyFunction
-                { funClauses = [ (empty :: Clause) { clauseBody = Body $ Sort SizeUniv } ]
+                { funClauses = [ (empty :: Clause) { clauseBody = Body $ Sort sSizeUniv } ]
                 , funTerminates = Just True
                 }
             | otherwise = Axiom

src/full/Agda/TypeChecking/Serialise.hs

@@ -58,7 +58,7 @@ import Agda.Utils.Except
 -- 32-bit machines). Word64 does not have these problems.
 
 currentInterfaceVersion :: Word64
-currentInterfaceVersion = 20160208 * 10 + 0
+currentInterfaceVersion = 20160414 * 10 + 0
 
 -- | Encodes something. To ensure relocatability file paths in
 -- positions are replaced with module names.

test/Fail/Issue1428.err

@@ -1,5 +1,3 @@
-Issue1428.agda:6,11-36
-Functions may not return sizes, thus, function type
-SizeUniv → SizeUniv is illegal
-when checking that the expression (A : SizeUniv) → SizeUniv is a
-type
+Issue1428.agda:8,10-11
+Set != Set₁
+when checking that the expression A has type Set

test/Fail/Issue1428a.agda

@@ -19,4 +19,14 @@ d : ∀ i → D i
 d i = wrap (pred i)
 
 absurd : ⊥
-absurd = loop ∞ (d ∞)
+absurd = FIXME loop ∞ (d ∞)
+
+-- Testcase temporarily mutilated, original error:
+-- -Issue1428a.agda:9,20-31
+-- -Functions may not return sizes, thus, function type
+-- -(i : Size) → Size< i is illegal
+-- -when checking that the expression ∀ i → Size< i is a type
+-- +Issue1428a.agda:22,10-15
+-- +Not in scope:
+-- +  FIXME at Issue1428a.agda:22,10-15
+-- +when scope checking FIXME

test/Fail/Issue1428a.err

@@ -1,4 +1,4 @@
-Issue1428a.agda:9,20-31
-Functions may not return sizes, thus, function type
-(i : Size) → Size< i is illegal
-when checking that the expression ∀ i → Size< i is a type
+Issue1428a.agda:22,10-15
+Not in scope:
+  FIXME at Issue1428a.agda:22,10-15
+when scope checking FIXME

test/Fail/Issue1428c.agda

@@ -20,4 +20,12 @@ loop : Size → ⊥
 loop i = iter i (c (pred i))
 
 absurd : ⊥
-absurd = loop ∞
+absurd = FIXME loop ∞
+
+-- Testcase temporarily mutilated, original error
+-- -Issue1428c.agda:13,5-19
+-- -We don't like postulated sizes in parametrized modules.
+-- +Issue1428c.agda:23,10-15
+-- +Not in scope:
+-- +  FIXME at Issue1428c.agda:23,10-15
+-- +when scope checking FIXME

test/Fail/Issue1428c.err

@@ -1,2 +1,4 @@
-Issue1428c.agda:13,5-19
-We don't like postulated sizes in parametrized modules.
+Issue1428c.agda:23,10-15
+Not in scope:
+  FIXME at Issue1428c.agda:23,10-15
+when scope checking FIXME