1 {-# LANGUAGE DataKinds #-}

2 {-# LANGUAGE MultiParamTypeClasses #-}

3 {-# LANGUAGE PolyKinds #-}

4 {-# LANGUAGE TypeFamilyDependencies #-}

5 {-# LANGUAGE UndecidableInstances #-}

6 {-# LANGUAGE ScopedTypeVariables #-}

7 {-# LANGUAGE NoMonomorphismRestriction #-}

11 {-

12 barapp2 :: Int

13 barapp2 = bar 1

15 bar :: Bar a -> Bar a

16 bar x = x

18 type family Bar a = r | r -> a where

19 Bar Int = Bool

20 Bar Bool = Int

21 Bar Bool = Char

23 type family F a b c = (result :: k) | result -> a b c

25 type family FClosed a b c = result | result -> a b c where

26 FClosed Int Char Bool = Bool

27 FClosed Char Bool Int = Int

28 FClosed Bool Int Char = Char

29 -}

30 {-

31 g6_use :: [Char]

32 g6_use = g6_id "foo"

34 g6_id :: G6 a -> G6 a

35 g6_id x = x

37 type family G6 a = r | r -> a

38 type instance G6 [a] = [Gi a]

39 type family Gi a = r | r -> a

40 type instance Gi Int = Char

41 -}

59 -- this is injective - a type variable introduced in the LHS is not mentioned on

60 -- RHS but we don't claim injectivity in that argument.

67 -- make sure we look through type synonyms...

71 -- .. but not newtypes

76 -- Closed type families

78 -- these are simple conversions from open type families. They should behave the

79 -- same

94 KClosed a = MaybeSyn a

96 -- Here the last equation might return both Int and Char but we have to

97 -- recognize that it is not possible due to equation overlap

101 Bak a = a

103 -- This is similar, except that the last equation contains concrete type. Since

104 -- it is overlapped it should be dropped with a warning

110 -- this one was tricky in the early implementation of injectivity. Now it is

111 -- identical to the above but we still keep it as a regression test.

117 -- Now let's use declared type families. All the below definitions should work

119 -- No ambiguity for any of the arguments - all are injective

121 f x = x

123 -- From 1st instance of F: a ~ Int, b ~ Char, c ~ Bool

127 -- now the closed variant of F

129 fc x = x

134 -- The last argument is not injective so it must be instantiated

136 i x = x

138 -- From 1st instance of I: a ~ Int, b ~ Char

142 -- again, closed variant of I

144 ic x = x

149 -- Now we have to test weird closed type families:

151 bak x = x

159 bakapp3 :: ()

163 foo x = x

169 bar x = x

177 -- Declarations below test more liberal RHSs of injectivity annotations:

178 -- permiting variables to appear in different order than the one in which they

179 -- were declared.

182 Hc a b = a b

186 -- repeated tyvars in the RHS of injectivity annotation: no warnings or errors

187 -- (consistent with behaviour for functional dependencies)

190 Jcx a b = a b

196 Kcx a b = a b

200 -- Declaring kind injectivity. Here we only claim that knowing the RHS

201 -- determines the LHS kind but not the type.

214 kproxy_id x = x

218 -- Now test some awkward cases from The Injectivity Paper. All should be

219 -- accepted.

220 type family Gx a

221 type family Hx a

243 g6_id x = x

248 -- A sole exception to "bare variables in the RHS" rule

252 -- This makes sure that over-saturated type family applications at the top-level

253 -- are accepted.

257 -- make sure we look through type synonyms properly

262 -- this has bare variable in the RHS but all LHS variables are also bare so it

263 -- should be accepted

267 -- Taken from #9587. This exposed a bug in the solver.

281 -- This used to fail during development