T6018failclosed.hs:11:5: error:
    Type family equation violates injectivity annotation.
    RHS of injective type family equation cannot be a type family:
      IdProxyClosed a = IdClosed a
    In the equations for closed type family ‘IdProxyClosed’
    In the type family declaration for ‘IdProxyClosed’

T6018failclosed.hs:19:5: error:
    Type family equation violates injectivity annotation.
    RHS of injective type family equation is a bare type variable
    but these LHS type and kind patterns are not bare variables: ‘'Z’
      PClosed 'Z m = m
    In the equations for closed type family ‘PClosed’
    In the type family declaration for ‘PClosed’

T6018failclosed.hs:19:5: error:
    Type family equations violate injectivity annotation:
      PClosed 'Z m = m
      PClosed ('S n) m = 'S (PClosed n m)
    In the equations for closed type family ‘PClosed’
    In the type family declaration for ‘PClosed’

T6018failclosed.hs:25:5: error:
    Type family equation violates injectivity annotation.
    Type and kind variables ‘k’, ‘b’
    cannot be inferred from the right-hand side.
    (enabling -fprint-explicit-kinds might help)
    In the type family equation:
    forall (k :: BOX) (k1 :: BOX) (b :: k) (c :: k1).
      JClosed Int b c = Char
    In the equations for closed type family ‘JClosed’
    In the type family declaration for ‘JClosed’

T6018failclosed.hs:30:5: error:
    Type family equation violates injectivity annotation.
    Type variable ‘n’ cannot be inferred from the right-hand side.
    In the type family equation:
      KClosed ('S n) m = 'S m
    In the equations for closed type family ‘KClosed’
    In the type family declaration for ‘KClosed’

T6018failclosed.hs:35:5: error:
    Type family equation violates injectivity annotation.
    RHS of injective type family equation cannot be a type family:
    forall (k :: BOX) (a :: k). LClosed a = MaybeSynClosed a
    In the equations for closed type family ‘LClosed’
    In the type family declaration for ‘LClosed’

T6018failclosed.hs:39:5: error:
    Type family equations violate injectivity annotation:
      FClosed Char Bool Int = Int
      FClosed Bool Int Char = Int
    In the equations for closed type family ‘FClosed’
    In the type family declaration for ‘FClosed’

T6018failclosed.hs:43:5: error:
    Type family equations violate injectivity annotation:
      IClosed Int Char Bool = Bool
      IClosed Int Int Int = Bool
    In the equations for closed type family ‘IClosed’
    In the type family declaration for ‘IClosed’

T6018failclosed.hs:50:3: error:
    Type family equation violates injectivity annotation.
    Type variable ‘a’ cannot be inferred from the right-hand side.
    In the type family equation:
      E2 a = 'False
    In the equations for closed type family ‘E2’
    In the type family declaration for ‘E2’

T6018failclosed.hs:61:3: error:
    Type family equations violate injectivity annotation:
      F a IO = IO a
      F Char b = b Int
    In the equations for closed type family ‘F’
    In the type family declaration for ‘F’

T6018failclosed.hs:66:5: error:
    Type family equation violates injectivity annotation.
    Kind variable ‘k’ cannot be inferred from the right-hand side.
    (enabling -fprint-explicit-kinds might help)
    In the type family equation:
    forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
    In the equations for closed type family ‘Gc’
    In the type family declaration for ‘Gc’