Order of constructor arguments matters for coverage checker

[GoogleCodeExporter]

-- Current Agda master.

{-# OPTIONS --no-coverage #-}
{-# OPTIONS -v tc.cover:20 #-}

open import Common.Bool
open import Common.Equality

_∨_ : Bool → Bool → Bool
a ∨ b = if a then true else b

module Works where
  data Term : Bool → Set where
    I   : Term false
    App : ∀ a b c → a ∨ b ≡ c → Term a → Term b → Term c

  -- The following clause works for the coverage checker:

  test : Term false → Set
  test (App false false .false refl I x) = Bool

module Fails where

  data Term : Bool -> Set where
    I   : Term false
    App : ∀ a b c → Term a → Term b → a ∨ b ≡ c → Term c

  -- If we put the equality proof later in App, it fails:

  test : Term false → Set
  test (App false false .false I x refl) = Bool
  -- The following checks, until you split at p.
  -- test (App false false .false I x p) = {!p!}

See also issue #408.

Original issue reported on code.google.com by andreas....@gmail.com on 6 Dec 2014 at 12:13

[GoogleCodeExporter]

Should it be possible to help Agda choose the argument splitting order?

I mean something similar to inferring arguments using dot pattern. So, when checker sees such pattern it doesn't try to split on the argument the
pattern is applied to.

Original comment by d.staro...@gmail.com on 7 Dec 2014 at 12:46

[UlfNorell]

This seems to be working now, although I have a bit of a hard time figuring out the expected behaviour due to --no-coverage.

[asr]

I added the above test case to the release-2.5.4 branch.