InjectiveTypeFamilies.hs

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE TypeFamilyDependencies     #-}
{-# LANGUAGE TypeFamilies     #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

module T6018 where

import T6018a -- defines G, identical to F

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

-- this is injective - a type variable introduced in the LHS is not mentioned on
-- RHS but we don't claim injectivity in that argument.
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)

-- make sure we look through type synonyms...
type family K a = r | r -> a
type instance K a = MaybeSyn a

-- .. but not newtypes
type family M a = r | r -> a
type instance M (Maybe a)    = MaybeSyn a
type instance M (MaybeNew a) = MaybeNew a

-- Closed type families

-- these are simple conversions from open type families. They should behave the
-- same
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

-- Here the last equation might return both Int and Char but we have to
-- recognize that it is not possible due to equation overlap
type family Bak a = r | r -> a where
     Bak Int  = Char
     Bak Char = Int
     Bak a    = a

-- This is similar, except that the last equation contains concrete type.  Since
-- it is overlapped it should be dropped with a warning
type family Foo a = r | r -> a where
    Foo Int  = Bool
    Foo Bool = Int
    Foo Bool = Bool

-- this one was tricky in the early implementation of injectivity.  Now it is
-- identical to the above but we still keep it as a regression test.
type family Bar a = r | r -> a where
    Bar Int  = Bool
    Bar Bool = Int
    Bar Bool = Char

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

-- No ambiguity for any of the arguments - all are injective
f :: F a b c -> F a b c
f x = x

-- From 1st instance of F: a ~ Int, b ~ Char, c ~ Bool
fapp :: Bool
fapp = f True

-- now the closed variant of F
fc :: FClosed a b c -> FClosed a b c
fc x = x

fcapp :: Bool
fcapp = fc True

-- The last argument is not injective so it must be instantiated
i :: I a b Int -> I a b Int
i x = x

-- From 1st instance of I: a ~ Int, b ~ Char
iapp :: Bool
iapp = i True

-- again, closed variant of I
ic :: IClosed a b Int -> IClosed a b Int
ic x = x

icapp :: Bool
icapp = ic True

-- Now we have to test weird closed type families:
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

-- Declarations below test more liberal RHSs of injectivity annotations:
-- permiting variables to appear in different order than the one in which they
-- were declared.
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

-- repeated tyvars in the RHS of injectivity annotation: no warnings or errors
-- (consistent with behaviour for functional dependencies)
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

-- Declaring kind injectivity. Here we only claim that knowing the RHS
-- determines the LHS kind but not the type.
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'

-- Now test some awkward cases from The Injectivity Paper.  All should be
-- accepted.
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"

-- A sole exception to "bare variables in the RHS" rule
type family Id (a :: k) = (result :: k) | result -> a
type instance Id a = a

-- This makes sure that over-saturated type family applications at the top-level
-- are accepted.
type family IdProxy (a :: k) b = r | r -> a
type instance IdProxy a b = (Id a) b

-- make sure we look through type synonyms properly
type IdSyn a = Id a
type family IdProxySyn (a :: k) b = r | r -> a
type instance IdProxySyn a b = (IdSyn a) b

-- this has bare variable in the RHS but all LHS varaiables are also bare so it
-- should be accepted
type family Fa (a :: k) (b :: k) = (r :: k2) | r -> k
type instance Fa a b = a

-- Taken from #9587. This exposed a bug in the solver.
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)

-- This used to fail during development
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