Declaration in irrelevant context (e.g. where modules) must be irrele…

…vant as well.

Fixes part of issue 610.

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

@@ -144,7 +144,10 @@ checkDecl d = do
 
 -- | Type check an axiom.
 checkAxiom :: Info.DefInfo -> Relevance -> QName -> A.Expr -> TCM ()
-checkAxiom i rel x e = do
+checkAxiom i rel0 x e = do
+  -- Andreas, 2012-04-18  if we are in irrelevant context, axioms is irrelevant
+  -- even if not declared as such (Issue 610).
+  rel <- max rel0 <$> asks envRelevance
   t <- isType_ e
   reportSDoc "tc.decl.ax" 10 $ sep
     [ text $ "checked type signature"

test/Common/Equality.agda

@@ -11,4 +11,7 @@ data _≡_ {a} {A : Set a} (x : A) : A → Set a where
 {-# BUILTIN REFL     refl #-}
 
 subst : ∀ {a p}{A : Set a}(P : A → Set p){x y : A} → x ≡ y → P x → P y
-subst P refl t = t
+subst P refl t = t
+
+cong : ∀ {a b}{A : Set a}{B : Set b}(f : A → B){x y : A} → x ≡ y → f x ≡ f y
+cong f refl = refl

test/fail/Issue610.agda

@@ -0,0 +1,36 @@
+-- Andreas, 2012-04-18, bug reported by pumpkingod
+module Issue610 where
+
+import Common.Level
+open import Common.Equality
+
+data ⊥ : Set where
+record ⊤ : Set where
+
+record A : Set₁ where
+  constructor set
+  field
+    .a : Set
+
+.get : A → Set
+get x = helper x
+  module R where
+  helper : .A -> Set
+  helper x = A.a x
+
+ack : A → Set
+ack x = R.helper x x
+
+hah : set ⊤ ≡ set ⊥
+hah = refl
+
+.moo : ⊥
+moo with cong ack hah
+moo | q = subst (λ x → x) q _
+
+baa : .⊥ → ⊥
+baa ()
+
+yoink : ⊥
+yoink = baa moo
+

test/fail/Issue610.err

@@ -0,0 +1,4 @@
+Issue610.agda:22,9-17
+Identifier R.helper is declared irrelevant, so it cannot be used
+here
+when checking that the expression R.helper x x has type Set