For example when implementing a `Show` instance for the following type:

```
data Shape = Circle Double
           | Box Vector2D
           | Polygon (List Vector2D)
           | Chain (List Vector2D)

```

...and omitting the `Chain` case, Idris will successfully type check this file.

Similar issues go for implementing other functions.

Adding `%default total` at the beginning of the file doesn't seem to help this, but my impression was that it should.