**Where is Agda's () pattern and what is `impossible`?**
**Where is Agda's () pattern and what is `impossible`?**
*(2012-01-26) `impossible` can be used to make sure that a clause does not get type checked
*`impossible` is a keyword used under certain circumstances to signal that a particular function pattern can never match. However, `impossible` cannot be used under all such circumstances, and is actually fairly limited. For the general case of proving that a particular pattern is impossible, construct a value of type _|_ and use `FalseElim` to return a value of the correct type.
For example,
`impossible` can only be used if the pattern it applies to cannot be unified. For example, in
```
f : (n : Nat) -> Vect n a -> Nat
...
f Z (_::_) impossible
f (S _) [] impossible
```
both "impossible" cases generate conflicting constraints for `n`: it must match both `S k` and `Z`.
`impossible` can't be used to implement functions like this:
```
g : a -> (a -> _|_) -> _|_
-- g _ _ impossible -- WRONG!
g a notA = notA a
```
Here, the impossibility is not caught by the compiler during the unification phase, so `impossible` doesn't work (and if you try, the compiler will complain that "this is a valid case"). Instead, we need to implement a function body.
foo : _|_ -> Unit
foo impossible
**Can't propositional arguments be made implicit?**
**Can't propositional arguments be made implicit?**
