{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
module T6018 where
import T6018a

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

type instance F Int Char Bool = Bool

type instance F Char Bool Int = Int

type instance F Bool Int Char = Char

type instance G Bool Int Char = Char

type family I (a :: k) b (c :: k) = r | r -> a b

type instance I Int Char Bool = Bool

type instance I Int Char Int = Bool

type instance I Bool Int Int = Int

type family J a (b :: k) = r | r -> a

type instance J Int b = Char

type MaybeSyn a = Maybe a

newtype MaybeNew a = MaybeNew (Maybe a)

type family K a = r | r -> a

type instance K a = MaybeSyn a

type family M a = r | r -> a

type instance M (Maybe a) = MaybeSyn a

type instance M (MaybeNew a) = MaybeNew a

type family FClosed a b c = result | result -> a b c where
        FClosed Int Char Bool = Bool
        FClosed Char Bool Int = Int
        FClosed Bool Int Char = Char

type family IClosed (a :: *) (b :: *) (c :: *) = r | r -> a b where
        IClosed Int Char Bool = Bool
        IClosed Int Char Int = Bool
        IClosed Bool Int Int = Int

type family JClosed a (b :: k) = r | r -> a where
        JClosed Int b = Char

type family KClosed a = r | r -> a where
        KClosed a = MaybeSyn a

type family Bak a = r | r -> a where
        Bak Int = Char
        Bak Char = Int
        Bak a = a

type family Foo a = r | r -> a where
        Foo Int = Bool
        Foo Bool = Int
        Foo Bool = Bool

type family Bar a = r | r -> a where
        Bar Int = Bool
        Bar Bool = Int
        Bar Bool = Char

f :: F a b c -> F a b c
f x = x

fapp :: Bool
fapp = f True

fc :: FClosed a b c -> FClosed a b c
fc x = x

fcapp :: Bool
fcapp = fc True

i :: I a b Int -> I a b Int
i x = x

iapp :: Bool
iapp = i True

ic :: IClosed a b Int -> IClosed a b Int
ic x = x

icapp :: Bool
icapp = ic True

bak :: Bak a -> Bak a
bak x = x

bakapp1 :: Char
bakapp1 = bak 'c'

bakapp2 :: Double
bakapp2 = bak 1.0

bakapp3 :: ()
bakapp3 = bak ()

foo :: Foo a -> Foo a
foo x = x

fooapp1 :: Bool
fooapp1 = foo True

bar :: Bar a -> Bar a
bar x = x

barapp1 :: Bool
barapp1 = bar True

barapp2 :: Int
barapp2 = bar 1

type family H a b = r | r -> b a

type family Hc a b = r | r -> b a where
        Hc a b = a b

class Hcl a b where
        type Ht a b = r | r -> b a

type family Jx a b = r | r -> a a

type family Jcx a b = r | r -> a a where
        Jcx a b = a b

class Jcl a b where
        type Jt a b = r | r -> a a

type family Kx a b = r | r -> a b b

type family Kcx a b = r | r -> a b b where
        Kcx a b = a b

class Kcl a b where
        type Kt a b = r | r -> a b b

type family L (a :: k1) = (r :: k2) | r -> k1 where
        L 'True = Int
        L 'False = Int
        L Maybe = 3
        L IO = 3

data KProxy (a :: *) = KProxy

type family KP (kproxy :: KProxy k) = r | r -> k

type instance KP ('KProxy :: KProxy Bool) = Int

type instance KP ('KProxy :: KProxy *) = Char

kproxy_id :: KP ('KProxy :: KProxy k) -> KP ('KProxy :: KProxy k)
kproxy_id x = x
kproxy_id_use = kproxy_id 'a'

type family Gx a

type family Hx a

type family Gi a = r | r -> a

type instance Gi Int = Char

type family Hi a = r | r -> a

type family F2 a = r | r -> a

type instance F2 [a] = [Gi a]

type instance F2 (Maybe a) = Hi a -> Int

type family F4 a = r | r -> a

type instance F4 [a] = (Gx a, a, a, a)

type instance F4 (Maybe a) = (Hx a, a, Int, Bool)

type family G2 a b = r | r -> a b

type instance G2 a Bool = (a, a)

type instance G2 Bool b = (b, Bool)

type family G6 a = r | r -> a

type instance G6 [a] = [Gi a]

type instance G6 Bool = Int

g6_id :: G6 a -> G6 a
g6_id x = x

g6_use :: [Char]
g6_use = g6_id "foo"

type family Id (a :: k) = (result :: k) | result -> a

type instance Id a = a

type family IdProxy (a :: k) b = r | r -> a

type instance IdProxy a b = (Id a) b

type IdSyn a = Id a

type family IdProxySyn (a :: k) b = r | r -> a

type instance IdProxySyn a b = (IdSyn a) b

type family Fa (a :: k) (b :: k) = (r :: k2) | r -> k

type instance Fa a b = a

type family Arr (repr :: * -> *) (a :: *) (b :: *) = (r :: *)
     | r -> repr a b

class ESymantics repr where
        int :: Int -> repr Int
        
        add :: repr Int -> repr Int -> repr Int
        
        lam :: (repr a -> repr b) -> repr (Arr repr a b)
        
        app :: repr (Arr repr a b) -> repr a -> repr b
te4
  = let c3 = lam (\ f -> lam (\ x -> f `app` (f `app` (f `app` x))))
      in (c3 `app` (lam (\ x -> x `add` int 14))) `app` (int 0)

class Manifold' a where
        type Base a = r | r -> a
        
        project :: a -> Base a
        
        unproject :: Base a -> a

id' :: forall a . (Manifold' a) => Base a -> Base a
id' = project . unproject