idris-lang/Idris-dev — pull request #1685 by soimort (2014-10-28 08:35:36+00:00)
Title: Add missing cases in checkUniqueKind (fixed #1606)

This PR fixes #1606. Currently `checkUniqueKind` breaks on type definitions such like:

```idr
Monoid_Unit : Type -> Type
Monoid_Unit carrier = carrier

data TypeUnit : (Monoid_Unit Type) where
MkTypeUnit : TypeUnit
```

(missing pattern for `App !(TT n) (TT n)`)

```idr
data Foo : Type where
bar : let x = Nat in x -> Foo
```

(missing pattern for `Bind n !(Binder (TT n)) (TT n)`)

`checkUniqueKind (UType UniqueType) _` should be a catch-all of `UniqueKindError`, and `checkUniqueKind _ _` lets pass the unique checking in all other cases (as this fixes #1606).