{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE CPP                   #-}
#if __GLASGOW_HASKELL__ < 806
{-# LANGUAGE TypeInType #-}
#endif
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE UndecidableInstances  #-}
#endif

module Data.Vinyl.TypeLevel where

import Data.Coerce
import Data.Kind

-- | A mere approximation of the natural numbers. And their image as lifted by
-- @-XDataKinds@ corresponds to the actual natural numbers.
data Nat = Z | S !Nat

-- | Produce a runtime 'Int' value corresponding to a 'Nat' type.
class NatToInt (n :: Nat) where
  natToInt :: Int

instance NatToInt 'Z where
  natToInt :: Int
natToInt = Int
0
  {-# INLINE natToInt #-}

instance NatToInt n => NatToInt ('S n) where
  natToInt :: Int
natToInt = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ NatToInt n => Int
forall (n :: Nat). NatToInt n => Int
natToInt @n
  {-# INLINE natToInt #-}

-- | Reify a list of type-level natural number indices as runtime
-- 'Int's relying on instances of 'NatToInt'.
class IndexWitnesses (is :: [Nat]) where
  indexWitnesses :: [Int]

instance IndexWitnesses '[] where
  indexWitnesses :: [Int]
indexWitnesses = []
  {-# INLINE indexWitnesses #-}

instance (IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) where
  indexWitnesses :: [Int]
indexWitnesses = NatToInt i => Int
forall (n :: Nat). NatToInt n => Int
natToInt @i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: IndexWitnesses is => [Int]
forall (is :: [Nat]). IndexWitnesses is => [Int]
indexWitnesses @is
  {-# INLINE indexWitnesses #-}

-- | Project the first component of a type-level tuple.
type family Fst (a :: (k1,k2)) where Fst '(x,y) = x

-- | Project the second component of a type-level tuple.
type family Snd (a :: (k1,k2)) where Snd '(x,y) = y

type family RLength xs where
  RLength '[] = 'Z
  RLength (x ': xs) = 'S (RLength xs)

-- | A partial relation that gives the index of a value in a list.
type family RIndex (r :: k) (rs :: [k]) :: Nat where
  RIndex r (r ': rs) = 'Z
  RIndex r (s ': rs) = 'S (RIndex r rs)

-- | A partial relation that gives the indices of a sublist in a larger list.
type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where
  RImage '[] ss = '[]
  RImage (r ': rs) ss = RIndex r ss ': RImage rs ss

-- | Remove the first occurence of a type from a type-level list.
type family RDelete r rs where
  RDelete r (r ': rs) = rs
  RDelete r (s ': rs) = s ': RDelete r rs

-- | A constraint-former which applies to every field in a record.
type family RecAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constraint where
  RecAll f '[] c = ()
  RecAll f (r ': rs) c = (c (f r), RecAll f rs c)

-- | Append for type-level lists.
type family (as :: [k]) ++ (bs :: [k]) :: [k] where
  '[] ++ bs = bs
  (a ': as) ++ bs = a ': (as ++ bs)

-- | Constraint that all types in a type-level list satisfy a
-- constraint.
type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint where
  AllConstrained c '[] = ()
  AllConstrained c (t ': ts) = (c t, AllConstrained c ts)

-- | Constraint that each Constraint in a type-level list is satisfied
-- by a particular type.
class AllSatisfied cs t where
instance AllSatisfied '[] t where
instance (c t, AllSatisfied cs t) => AllSatisfied (c ': cs) t where

-- | Constraint that all types in a type-level list satisfy each
-- constraint from a list of constraints.
--
-- @AllAllSat cs ts@ should be equivalent to @AllConstrained
-- (AllSatisfied cs) ts@ if partial application of type families were
-- legal.
type family AllAllSat cs ts :: Constraint where
  AllAllSat cs '[] = ()
  AllAllSat cs (t ': ts) = (AllSatisfied cs t, AllAllSat cs ts)

-- | Apply a type constructor to a record index. Record indexes are
-- either 'Type' or @('Symbol', 'Type')@. In the latter case, the type
-- constructor is applied to the second component of the tuple.
type family ApplyToField (t :: Type -> Type) (a :: k1) = (r :: k1) | r -> t a where
  ApplyToField t '(s,x) = '(s, t x)
  ApplyToField t x = t x

-- | Apply a type constructor to each element of a type level list
-- using 'ApplyOn'.
type family MapTyCon t xs = r | r -> xs where
  MapTyCon t '[] = '[]
  MapTyCon t (x ': xs) = ApplyToField t x ': MapTyCon t xs

-- | This class is used for `consMatchCoercion` with older versions
-- of GHC.
class Coercible (f x) (g x) => Similar f g (x :: k)
instance Coercible (f x) (g x) => Similar f g (x :: k)