1 {-# LANGUAGE TypeFamilyDependencies, DataKinds, PolyKinds,

2 UndecidableInstances #-}

5 -- Id is injective...

7 IdClosed a = a

9 -- ...but despite that we disallow a call to Id

11 IdProxyClosed a = IdClosed a

15 -- PClosed is not injective, although the user declares otherwise. This

16 -- should be rejected on the grounds of calling a type family in the

17 -- RHS.

19 PClosed Z m = m

22 -- this is not injective - not all injective type variables mentioned

23 -- on LHS are mentioned on RHS

27 -- this is not injective - not all injective type variables mentioned

28 -- on LHS are mentioned on RHS (tyvar is now nested inside a tycon)

32 -- hiding a type family application behind a type synonym should be rejected

35 LClosed a = MaybeSynClosed a

52 -- This exposed a subtle bug in the implementation during development. After

53 -- unifying the RHS of (1) and (2) the LHS substitution was done only in (2)

54 -- which made it look like an overlapped equation. This is not the case and this

55 -- definition should be rejected. The first two equations are here to make sure

56 -- that the internal implementation does list indexing corrcectly (this is a bit

57 -- tricky because the list is kept in reverse order).

64 -- This should fail because there is no way to determine a, b and k from the RHS