:set -XTypeFamilyDependencies
:set -XDataKinds
:set -XUndecidableInstances
:set -XPolyKinds
:set -XMultiParamTypeClasses

-- IA = injectivity annotation `| foo -> bar`

-- use incorrect tyvar in LHS of IA
type family F a = r | a -> a
type family Fc a = r | a -> a where { Fc a = a }
class Fcl a where { type Ft a = r | a -> a }

-- declare result tyvar to be duplicate (without IA)
type family G a = a
type family Gc a = a where { Gc a = a }

-- declare result tyvar to be duplicate (with IA)
type family Gb a = a | a -> a
type family Gcb a = a | a -> a where { Gcb a = a }
class Gclb a where { type Gtb a = a | a -> a } -- here we want two errors

-- not in-scope tyvar in RHS of IA
type family I a b = r | r -> c
type family Ic a b = r | r -> c where { Ic a b = a }
class Icl a b where { type It a b = r | r -> c }

-- repeated tyvar on RHS of IA
type family J a b = r | r -> a a
type family Jc a b = r | r -> a a where { Jc a b = a }
class Jcl a b where { type Jt a b = r | r -> a a }

-- not in-scope tyvar in LHS of IA
type family L a b = r | c -> a
type family Lc a b = r | c -> a where { Lc a b = a }
class Lcl a b where { type Lt a b = r | c -> a }

-- result variable shadows variable in class head
class M a b where { type Mt b = a | a -> b }

-- here b is out-of-scope
class N a b where { type Nt a = r | r -> a b }