content: {-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances, PolyKinds,
               MultiParamTypeClasses, FlexibleInstances #-}
  
  module T6018fail where
  
  import T6018Afail -- defines G, identical to F
  import T6018Cfail -- imports H from T6018Bfail, defines some equations for H
  import T6018Dfail -- imports H from T6018Bfail, defines conflicting eqns
  
  type family F a b c = (result :: *) | result -> a b c
  type instance F Int  Char Bool = Bool
  type instance F Char Bool Int  = Int
  type instance F Bool Int  Char = Int
  
  type instance G Bool Int  Char = Int
  
  type family I a b c = r | r -> a b
  type instance I Int  Char Bool = Bool
  type instance I Int  Int  Int  = Bool
  type instance I Bool Int  Int  = Int
  
  -- Id is injective...
  type family Id a = result | result -> a
  type instance Id a = a
  
  -- ...but despite that we disallow a call to Id
  type family IdProxy a = r | r -> a
  type instance IdProxy a = Id a
  
  data N = Z | S N
  
  -- P is not injective, although the user declares otherwise. This
  -- should be rejected on the grounds of calling a type family in the
  -- RHS.
  type family P (a :: N) (b :: N) = (r :: N) | r -> a b
  type instance P  Z    m = m
  type instance P (S n) m = S (P n m)
  
  -- this is not injective - not all injective type variables mentioned
  -- on LHS are mentioned on RHS
  type family J a b c = r | r -> a b
  type instance J Int b c = Char
  
  -- same as above, but tyvar is now nested inside a tycon
  type family K (a :: N) (b :: N) = (r :: N) | r -> a b
  type instance K (S n) m = S m
  
  -- Make sure we look through type synonyms to catch errors
  type MaybeSyn a = Id a
  type family L a = r | r -> a
  type instance L a = MaybeSyn a
  
  -- These should fail because given the RHS kind there is no way to determine LHS
  -- kind
  class PolyKindVarsC a where
      type PolyKindVarsF a = (r :: k) | r -> a
  
  instance PolyKindVarsC '[] where
      type PolyKindVarsF '[] = '[]
  
  type family PolyKindVars (a :: k0) = (r :: k1) | r -> a
  type instance PolyKindVars '[] = '[]
  
  -- This should fail because there is no way to determine k from the RHS
  type family Fc (a :: k) (b :: k) = r | r -> k
  type instance Fc a b = Int
  
  -- This should fail because there is no way to determine a, b and k from the RHS
  type family Gc (a :: k) (b :: k) = r | r -> a b
  type instance Gc a b = Int
  
  -- fails because injectivity is not compositional in this case
  type family F1 a = r | r -> a
  type instance F1 [a]       = Maybe (GF1 a)
  type instance F1 (Maybe a) = Maybe (GF2 a)
  
  type family GF1 a = r | r -> a
  type instance GF1 Int = Bool
  
  type family GF2 a = r | r -> a
  type instance GF2 Int = Bool
  
  type family HF1 a
  type instance HF1 Bool = Bool
  
  type family W1 a = r | r -> a
  type instance W1 [a] = a
  
  type family W2 a = r | r -> a
  type instance W2 [a] = W2 a
  
  -- not injective because of infinite types
  type family Z1 a = r | r -> a
  type instance Z1 [a]       = (a, a)
  type instance Z1 (Maybe b) = (b, [b])
  
  type family G1 a = r | r -> a
  type instance G1 [a]       = [a]
  type instance G1 (Maybe b) = [(b, b)]
  
  type family G3 a b = r | r -> b
  type instance G3 a Int  = (a, Int)
  type instance G3 a Bool = (Bool, a)
  
  type family G4 a b = r | r -> a b
  type instance G4 a b = [a]
  
  type family G5 a = r | r -> a
  type instance G5 [a] = [GF1 a] -- GF1 injective
  type instance G5 Int = [Bool]
  
  type family G6 a = r | r -> a
  type instance G6 [a]  = [HF1 a] -- HF1 not injective
  type instance G6 Bool = Int
  
  type family G7a a b (c :: k) = r | r -> a b
  type family G7 a b (c :: k) = r | r -> a b c
  type instance G7 a b c = [G7a a b c]
  
  class C a b where
      type FC a (b :: *) = r | r -> b
      type instance FC a b = b
  
  instance C Int Char where
      type FC Int Char = Bool
  
  -- this should fail because the default instance conflicts with one of the
  -- earlier instances
  instance C Int Bool {- where
      type FC Int Bool = Bool-}
  
  -- and this should fail because it violates "bare variable in the RHS"
  -- restriction
  instance C Char a
  