1{-# LANGUAGE DataKinds #-} 2{-# LANGUAGE MultiParamTypeClasses #-} 3{-# LANGUAGE PolyKinds #-} 4{-# LANGUAGE TypeFamilyDependencies #-} 5{-# LANGUAGE TypeFamilies #-} 6{-# LANGUAGE UndecidableInstances #-} 7{-# LANGUAGE ScopedTypeVariables #-} 8{-# LANGUAGE NoMonomorphismRestriction #-} 9 10module T6018 where 11 12import T6018a -- defines G, identical to F 13 14type family F a b c = (result :: k) | result -> a b c 15type instance F Int Char Bool = Bool 16type instance F Char Bool Int = Int 17type instance F Bool Int Char = Char 18 19 20type instance G Bool Int Char = Char 21 22type family I (a :: k) b (c :: k) = r | r -> a b 23type instance I Int Char Bool = Bool 24type instance I Int Char Int = Bool 25type instance I Bool Int Int = Int 26 27-- this is injective - a type variable introduced in the LHS is not mentioned on 28-- RHS but we don't claim injectivity in that argument. 29type family J a (b :: k) = r | r -> a 30type instance J Int b = Char 31 32type MaybeSyn a = Maybe a 33newtype MaybeNew a = MaybeNew (Maybe a) 34 35-- make sure we look through type synonyms... 36type family K a = r | r -> a 37type instance K a = MaybeSyn a 38 39-- .. but not newtypes 40type family M a = r | r -> a 41type instance M (Maybe a) = MaybeSyn a 42type instance M (MaybeNew a) = MaybeNew a 43 44-- Closed type families 45 46-- these are simple conversions from open type families. They should behave the 47-- same 48type family FClosed a b c = result | result -> a b c where 49 FClosed Int Char Bool = Bool 50 FClosed Char Bool Int = Int 51 FClosed Bool Int Char = Char 52 53type family IClosed (a :: *) (b :: *) (c :: *) = r | r -> a b where 54 IClosed Int Char Bool = Bool 55 IClosed Int Char Int = Bool 56 IClosed Bool Int Int = Int 57 58type family JClosed a (b :: k) = r | r -> a where 59 JClosed Int b = Char 60 61type family KClosed a = r | r -> a where 62 KClosed a = MaybeSyn a 63 64-- Here the last equation might return both Int and Char but we have to 65-- recognize that it is not possible due to equation overlap 66type family Bak a = r | r -> a where 67 Bak Int = Char 68 Bak Char = Int 69 Bak a = a 70 71-- This is similar, except that the last equation contains concrete type. Since 72-- it is overlapped it should be dropped with a warning 73type family Foo a = r | r -> a where 74 Foo Int = Bool 75 Foo Bool = Int 76 Foo Bool = Bool 77 78-- this one was tricky in the early implementation of injectivity. Now it is 79-- identical to the above but we still keep it as a regression test. 80type family Bar a = r | r -> a where 81 Bar Int = Bool 82 Bar Bool = Int 83 Bar Bool = Char 84 85-- Now let's use declared type families. All the below definitions should work 86 87-- No ambiguity for any of the arguments - all are injective 88f :: F a b c -> F a b c 89f x = x 90 91-- From 1st instance of F: a ~ Int, b ~ Char, c ~ Bool 92fapp :: Bool 93fapp = f True 94 95-- now the closed variant of F 96fc :: FClosed a b c -> FClosed a b c 97fc x = x 98 99fcapp :: Bool 100fcapp = fc True 101 102-- The last argument is not injective so it must be instantiated 103i :: I a b Int -> I a b Int 104i x = x 105 106-- From 1st instance of I: a ~ Int, b ~ Char 107iapp :: Bool 108iapp = i True 109 110-- again, closed variant of I 111ic :: IClosed a b Int -> IClosed a b Int 112ic x = x 113 114icapp :: Bool 115icapp = ic True 116 117-- Now we have to test weird closed type families: 118bak :: Bak a -> Bak a 119bak x = x 120 121bakapp1 :: Char 122bakapp1 = bak 'c' 123 124bakapp2 :: Double 125bakapp2 = bak 1.0 126 127bakapp3 :: () 128bakapp3 = bak () 129 130foo :: Foo a -> Foo a 131foo x = x 132 133fooapp1 :: Bool 134fooapp1 = foo True 135 136bar :: Bar a -> Bar a 137bar x = x 138 139barapp1 :: Bool 140barapp1 = bar True 141 142barapp2 :: Int 143barapp2 = bar 1 144 145-- Declarations below test more liberal RHSs of injectivity annotations: 146-- permiting variables to appear in different order than the one in which they 147-- were declared. 148type family H a b = r | r -> b a 149type family Hc a b = r | r -> b a where 150 Hc a b = a b 151class Hcl a b where 152 type Ht a b = r | r -> b a 153 154-- repeated tyvars in the RHS of injectivity annotation: no warnings or errors 155-- (consistent with behaviour for functional dependencies) 156type family Jx a b = r | r -> a a 157type family Jcx a b = r | r -> a a where 158 Jcx a b = a b 159class Jcl a b where 160 type Jt a b = r | r -> a a 161 162type family Kx a b = r | r -> a b b 163type family Kcx a b = r | r -> a b b where 164 Kcx a b = a b 165class Kcl a b where 166 type Kt a b = r | r -> a b b 167 168-- Declaring kind injectivity. Here we only claim that knowing the RHS 169-- determines the LHS kind but not the type. 170type family L (a :: k1) = (r :: k2) | r -> k1 where 171 L 'True = Int 172 L 'False = Int 173 L Maybe = 3 174 L IO = 3 175 176data KProxy (a :: *) = KProxy 177type family KP (kproxy :: KProxy k) = r | r -> k 178type instance KP ('KProxy :: KProxy Bool) = Int 179type instance KP ('KProxy :: KProxy *) = Char 180 181kproxy_id :: KP ('KProxy :: KProxy k) -> KP ('KProxy :: KProxy k) 182kproxy_id x = x 183 184kproxy_id_use = kproxy_id 'a' 185 186-- Now test some awkward cases from The Injectivity Paper. All should be 187-- accepted. 188type family Gx a 189type family Hx a 190type family Gi a = r | r -> a 191type instance Gi Int = Char 192type family Hi a = r | r -> a 193 194type family F2 a = r | r -> a 195type instance F2 [a] = [Gi a] 196type instance F2 (Maybe a) = Hi a -> Int 197 198type family F4 a = r | r -> a 199type instance F4 [a] = (Gx a, a, a, a) 200type instance F4 (Maybe a) = (Hx a, a, Int, Bool) 201 202type family G2 a b = r | r -> a b 203type instance G2 a Bool = (a, a) 204type instance G2 Bool b = (b, Bool) 205 206type family G6 a = r | r -> a 207type instance G6 [a] = [Gi a] 208type instance G6 Bool = Int 209 210g6_id :: G6 a -> G6 a 211g6_id x = x 212 213g6_use :: [Char] 214g6_use = g6_id "foo" 215 216-- A sole exception to "bare variables in the RHS" rule 217type family Id (a :: k) = (result :: k) | result -> a 218type instance Id a = a 219 220-- This makes sure that over-saturated type family applications at the top-level 221-- are accepted. 222type family IdProxy (a :: k) b = r | r -> a 223type instance IdProxy a b = (Id a) b 224 225-- make sure we look through type synonyms properly 226type IdSyn a = Id a 227type family IdProxySyn (a :: k) b = r | r -> a 228type instance IdProxySyn a b = (IdSyn a) b 229 230-- this has bare variable in the RHS but all LHS varaiables are also bare so it 231-- should be accepted 232type family Fa (a :: k) (b :: k) = (r :: k2) | r -> k 233type instance Fa a b = a 234 235-- Taken from #9587. This exposed a bug in the solver. 236type family Arr (repr :: * -> *) (a :: *) (b :: *) = (r :: *) | r -> repr a b 237 238class ESymantics repr where 239 int :: Int -> repr Int 240 add :: repr Int -> repr Int -> repr Int 241 242 lam :: (repr a -> repr b) -> repr (Arr repr a b) 243 app :: repr (Arr repr a b) -> repr a -> repr b 244 245te4 = let c3 = lam (\f -> lam (\x -> f `app` (f `app` (f `app` x)))) 246 in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0) 247 248-- This used to fail during development 249class Manifold' a where 250 type Base a = r | r -> a 251 project :: a -> Base a 252 unproject :: Base a -> a 253 254id' :: forall a. ( Manifold' a ) => Base a -> Base a 255id' = project . unproject 256