Remove --no-coverage-check option

[asr]

{-# OPTIONS --no-coverage-check #-}

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

id : ℕ → ℕ
id (succ n) = succ n

z : ℕ
z = id zero

-- When normalising `z` (C-c C-n), I got
--
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/CompiledClause/Match.hs:191

-- Tested with 2.4.2.5 and master.

[UlfNorell]

Is there a good reason to keep --no-coverage-check, or can we just remove it?

[asr]

If you remove --no-coverage-check you get an error due to the missing pattern matching id zero in the definition of id.

Edit (2016-03-28). After reread Ulf's comment and my answer, I don't know what I was thinking...

[UlfNorell]

Which is what you would expect. What I mean is, are there legitimate cases where --no-coverage-check makes sense? It's quite easy to emulate it with a catch-all and a postulate.

[asr]

What I mean is, are there legitimate cases where --no-coverage-check makes sense?

Good question! I don't know any legitimate example.

[andreasabel]

Before Nisse @nad insisted to make this an internal error, there was an error like "Incomplete matching for function id" triggered by "id zero". However, from our perspective in only arose for Agda bugs, as no one used --no-coverage-check.
I think --no-coverage-check could go to the attic, but it might be worthwhile asking on the Agda list first.

[asr]

I think --no-coverage-check could go to the attic, but it might be worthwhile asking on the Agda list first.

No one requested the option, so I'll remove it.

[asr]

Relevant for #1845.