[Agda] Compile-time parsing

[Dominique Devriese]

All,

2011/12/16 Conor McBride <conor at strictlypositive.org>:
> How about treating as an error an unsolved meta whose type, were it an
> hypothesis, would be dismissed by an absurd pattern?

That would mean the following

  id : (t : ⊥) → ⊥
  id v = _

would also result in an error, right? And more complex examples where
you prove that things are not true?

What about a special data type

  data TypeError (errMsg : String) where

which is special cased during type checking such that an unsolved meta
of this type would result in a type error with the given error
message. For example:

  open import Data.Fin hiding (#_)
  open import Data.Nat renaming (_≤?_ to _N≤?_; _<_ to _N<_)
  open import Data.Nat.Show
  open import Data.String
  open import Data.Bool
  open import Data.Unit
  open import Relation.Nullary
  open import Relation.Nullary.Decidable

  assert : String → Bool → Set
  assert _ true = ⊤
  assert s false = TypeError s

  assertDec : ∀ {p} {P : Set p} → String → Dec P → Set
  assertDec s d = assert s ⌊ d ⌋

  assertToWitness : ∀ {p s} {P : Set p} {Q : Dec P} → assertDec s Q → P
  assertToWitness {Q = yes p} _  = p
  assertToWitness {Q = no  _} ()

  #_ : ∀ m {n} {m<n : assertDec (show m ++ " should be strictly
smaller than " ++ show n) (suc m N≤? n)} → Fin n
  #_ _ {m<n = m<n} = fromℕ≤ (assertToWitness m<n)

  -- type error "3 should be strictly smaller than 2"
  test : Fin 2
  test = # 3

Dominique