{-# 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