[ fix agda#1063 ] Freeze all metas after checking module telescope

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

@@ -788,7 +788,13 @@ checkTypeSignature _ = __IMPOSSIBLE__   -- type signatures are always axioms
 -- | Type check a module.
 
 checkSection :: Info.ModuleInfo -> ModuleName -> A.GeneralizeTelescope -> [A.Declaration] -> TCM ()
-checkSection _ x tel ds = newSection x tel $ mapM_ checkDeclCached ds
+checkSection _ x tel ds = newSection x tel $ do
+  -- Jesper, 2018-12-02, Issue #1063: definitions inside a module
+  -- shouldn't influence the types of the module parameters.
+  solveSizeConstraints DefaultToInfty
+  _ <- freezeMetas
+
+  mapM_ checkDeclCached ds
 
 
 -- | Helper for 'checkSectionApplication'.

test/Fail/Issue1063.agda

@@ -0,0 +1,10 @@
+-- Jesper, 2018-12-02, Issue #1063: Since we freeze metavariables
+-- after each declaration, it only makes sense to also freeze metas
+-- *before* the first declaration in a module.
+
+module _ where
+
+module M (A : _) where
+
+  x : Set
+  x = A

test/Fail/Issue1063.err

@@ -0,0 +1,7 @@
+Failed to solve the following constraints:
+  _2 := λ A → A [blocked on problem 1]
+  [1] _1 =< Set : _0
+  _0 = Set₁
+Unsolved metas at the following locations:
+  Issue1063.agda:7,15-16
+  Issue1063.agda:10,7-8

test/Fail/Issue3274.agda

@@ -23,10 +23,10 @@ meta : Nat
 meta = _
 
 -- `n` gets pruned due to the meta == suc n constraint, so we can't generalize over it
-module _ (X : Set) where
-  tricky : let n = _
-               _ = solve meta == suc n by refl
-           in IsHead {n = n} x xs → Nat
-  tricky h = 0
+tricky : (X : Set)
+       → let n = _
+             _ = solve meta == suc n by refl
+         in IsHead {n = n} x xs → Nat
+tricky X h = 0
 
 mutual-block = Nat

test/Fail/Issue3274.err

@@ -1,2 +1,2 @@
 Unsolved metas at the following locations:
-  Issue3274.agda:27,20-21
+  Issue3274.agda:27,18-19

test/Fail/Issue921.agda

@@ -1,5 +1,4 @@
 {-# OPTIONS --without-K #-}
-{-# OPTIONS --allow-unsolved-metas #-}
 
 -- This issue demonstrates that a failing termination check,
 -- subsequently blocking reductions, makes some `impossible'

test/interaction/Issue1353.agda

@@ -54,7 +54,7 @@ P ⊆ Q = ∀ {x} → P x → Q x
 Alg : ∀ {O} → O ▷ O → Pow O → Set
 Alg Σ X = ⟦ Σ ⟧ X ⊆ X
 
-module _ {I₁ I₂ O₁ O₂} where
+module _ {I₁ I₂ O₁ O₂ : Set} where
 
   record ContainerMorphism
          (C₁ : I₁ ▷ O₁) (C₂ : I₂ ▷ O₂)

test/interaction/Issue1353.out

@@ -3,7 +3,7 @@
 (agda2-highlight-clear)
 (agda2-verbose "Found interaction point ?0 : (Pow I) ")
 (agda2-status-action "ShowImplicit")
-(agda2-info-action "*All Goals, Errors*" "?0 : Pow I _239 : (a : Arity Ω {i} p) → _X_241 {Ψ = X} {X = i} (m = (input Ω {i} p a)) [ at Issue1353.agda:89,71-72 ] _240 : (a : Arity Ω {i} p) → _X_241 {Ψ = X} {X = i} (m = (input Ω {i} p a)) [ at Issue1353.agda:89,71-72 ] _X_241 : Set [ at Issue1353.agda:89,60-65 ] _242 : Σ (Parameter Ψ i) (λ p → (a : Arity Ψ {i} p) → X (input Ψ {i} p a)) [ at Issue1353.agda:89,54-73 ] _243 : Σ (Parameter Ψ i) (λ p → (a : Arity Ψ {i} p) → X (input Ψ {i} p a)) [ at Issue1353.agda:89,54-73 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _242 := λ {I} {Ω} {Ψ} {X} φ m {i} p k → ⟪_⟫ {I} {Ω} {Ψ} m (λ v → _X_241 {I = I} {Ψ = X} {X = i} (m = v)) {i} (p , _240 {I = I} {Ω = Ω} {Ψ = Ψ} {X = X} (φ = φ) (m = m) {i = i} (p = p) (k = k)) [blocked on problem 368] [366] X (input Ω {i} p a) =< _X_241 {Ψ = X} {X = i} (m = (input Ω {i} p a)) : Set [368, 370] _X_241 {Ψ = X} {X = i} (m = (input Ψ {i} x a)) =< X (input Ψ {i} x a) : Set _239 := λ {I} {Ω} {Ψ} {X} φ m {i} p k → k [blocked on problem 366] " nil)
+(agda2-info-action "*All Goals, Errors*" "?0 : Pow I _231 : (a : Arity Ω {i} p) → _X_233 {Ψ = X} {X = i} (m = (input Ω {i} p a)) [ at Issue1353.agda:89,71-72 ] _232 : (a : Arity Ω {i} p) → _X_233 {Ψ = X} {X = i} (m = (input Ω {i} p a)) [ at Issue1353.agda:89,71-72 ] _X_233 : Set [ at Issue1353.agda:89,60-65 ] _234 : Σ (Parameter Ψ i) (λ p → (a : Arity Ψ {i} p) → X (input Ψ {i} p a)) [ at Issue1353.agda:89,54-73 ] _235 : Σ (Parameter Ψ i) (λ p → (a : Arity Ψ {i} p) → X (input Ψ {i} p a)) [ at Issue1353.agda:89,54-73 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _234 := λ {I} {Ω} {Ψ} {X} φ m {i} p k → ⟪_⟫ {I} {Ω} {Ψ} m (λ v → _X_233 {I = I} {Ψ = X} {X = i} (m = v)) {i} (p , _232 {I = I} {Ω = Ω} {Ψ = Ψ} {X = X} (φ = φ) (m = m) {i = i} (p = p) (k = k)) [blocked on problem 368] [366] X (input Ω {i} p a) =< _X_233 {Ψ = X} {X = i} (m = (input Ω {i} p a)) : Set [368, 370] _X_233 {Ψ = X} {X = i} (m = (input Ψ {i} x a)) =< X (input Ψ {i} x a) : Set _231 := λ {I} {Ω} {Ψ} {X} φ m {i} p k → k [blocked on problem 366] " nil)
 ((last . 1) . (agda2-goals-action '(0)))
 (agda2-give-action 0 "X")
 (agda2-status-action "ShowImplicit")

test/interaction/Issue2751.out

@@ -27,5 +27,5 @@
 (agda2-highlight-add-annotations 'nil '(1 36 (comment) t) '(37 77 (comment) t) '(648 673 (comment) t) '(677 734 (comment) t) '(738 785 (comment) t) '(826 832 (keyword) t) '(898 912 (comment) t) '(965 979 (comment) t))
 (agda2-highlight-add-annotations 'nil '(623 645 (unsolvedconstraint)) '(839 840 (unsolvedmeta)) '(885 896 (unsolvedconstraint)) '(952 963 (unsolvedconstraint)))
 (agda2-status-action "")
-(agda2-info-action "*All Goals, Errors*" "_28 : ;Agda.Primitive.Level [ at Issue2751.agda:42,7-8 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _28 =< ;Agda.Primitive.lsuc ;Agda.Primitive.lzero a =< _28 [55, 56] size t =< i : Size [49, 50] i =< size t : Size " nil)
+(agda2-info-action "*All Goals, Errors*" "_28 : ;Agda.Primitive.Level [ at Issue2751.agda:42,7-8 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: _28 =< ;Agda.Primitive.lsuc ;Agda.Primitive.lzero a =< _28 [49, 50] i =< size t : Size [55, 56] size t =< i : Size " nil)
 ((last . 1) . (agda2-goals-action '()))

test/interaction/Issue564.agda

@@ -5,7 +5,7 @@ open import Agda.Primitive using (Level) renaming (lzero to zero)
 postulate
   A : Level → Set
 
-module M ℓ where
+module M (ℓ : Level) where
   postulate a : A ℓ
 
 postulate