[ fix #3853 ] Set quantity to infinity in codomain of pi type

agda · Jun 13, 2019 · 37e8d81 · 37e8d81
1 parent 20097f6
commit 37e8d81
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 3 deletions.
diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs b/src/full/Agda/TypeChecking/Rules/Term.hs
@@ -291,7 +291,7 @@ checkTypedBindings lamOrPi (A.TBind r xs' e) ret = do
         OutputTypeNameNotYetKnown{} -> return ()
         NoOutputTypeName -> warning . InstanceNoOutputTypeName =<< prettyTCM (A.TBind r ixs e)
 
-    let xs' = (map . mapRelevance) (modRel lamOrPi experimental) xs
+    let xs' = map (modMod lamOrPi experimental) xs
     addContext (xs', t) $
       ret $ namedBindsToTel xs t
     where
@@ -301,8 +301,9 @@ checkTypedBindings lamOrPi (A.TBind r xs' e) ret = do
         -- modify the new context entries
         modEnv LamNotPi = workOnTypes
         modEnv _        = id
-        modRel PiNotLam xp = if xp then irrToNonStrict else id
-        modRel _        _  = id
+        modMod PiNotLam xp = (if xp then mapRelevance irrToNonStrict else id)
+                           . (setQuantity Quantityω)
+        modMod _        _  = id
 checkTypedBindings lamOrPi (A.TLet _ lbs) ret = do
     checkLetBindings lbs (ret EmptyTel)
 

diff --git a/test/Succeed/Issue3853.agda b/test/Succeed/Issue3853.agda
@@ -0,0 +1,5 @@
+postulate
+  A : Set
+  B : A → Set
+
+T = (@0 x : A) → B x