ActuallyDep.hs

{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE DeriveFoldable           #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE FunctionalDependencies   #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}

module Main where

import           Data.Bifunctor
import           Data.Functor
import           Data.Kind
import           Data.List
import           Data.Maybe
import           Data.Type.Bool
import           Data.Type.Equality
import           Data.Typeable
import           GHC.Exts
import           GHC.TypeLits

infix 4 ===
type (===) :: forall a b. a -> b -> Bool
type family x === y where
    x === x = 'True
    x === y = 'False

type TryUnify :: forall a b. Bool -> a -> b -> Constraint
class same ~ (x === y) => TryUnify same x y
instance (x === y) ~ 'False => TryUnify 'False x y
instance {-# INCOHERENT #-} (x ~~ y, same ~ 'True) => TryUnify same x y

type (~?~) :: forall a b. a -> b -> Constraint
type x ~?~ y = TryUnify (x === y) x y

type Var :: forall k. Nat -> k
data family Var i

type ArgOf :: forall a b. b -> a
type family ArgOf y where
    ArgOf (_ x) = x

type TryDiscriminate :: forall a b. Bool -> Bool -> a -> b -> Constraint
class TryDiscriminate same diff x y | same -> diff
instance {-# INCOHERENT #-} diff ~ 'True => TryDiscriminate same diff x y
instance diff ~ 'False => TryDiscriminate 'True diff x y

-- type Solidify :: forall b. b -> Constraint
-- class Solidify y
-- instance {-# OVERLAPPING #-} Solidify (Var i)
-- instance {-# OVERLAPPING #-} rep ~ LiftedRep => Solidify (TYPE rep)
-- instance {-# OVERLAPPABLE #-} (Solidify f, Solidify x) => Solidify (f x)
-- instance {-# INCOHERENT #-}
--      ( Solidify b
--      , i ~ ArgOf @Nat y
--      , var ~ (Var i :: b)
--      , y ~?~ var
--      ) => Solidify (y :: b)

-- type EnumerateFromTo :: forall b. Nat -> Nat -> b -> Constraint
-- class EnumerateFromTo i j y | i y -> j
-- instance {-# OVERLAPPING #-} i ~ j => EnumerateFromTo i j *
-- instance {-# OVERLAPPING #-} i ~ j => EnumerateFromTo i j (->)
-- instance {-# OVERLAPPING #-}
--     ( EnumerateFromTo i j b
--     , l ~?~ j
--     , k ~ If (l === j) (j + 1) j
--     ) => EnumerateFromTo i k (Var l :: b)
-- instance {-# OVERLAPS #-}
--     ( EnumerateFromTo i j f
--     , EnumerateFromTo j k x
--     ) => EnumerateFromTo i k (f x)
-- instance {-# OVERLAPPABLE #-} EnumerateFromTo i j b => EnumerateFromTo i j (y :: b)

type EnumerateFromTo :: forall b. Nat -> Nat -> b -> Constraint
class EnumerateFromTo i j y | i y -> j
instance {-# OVERLAPPABLE #-}
    ( EnumerateFromTo i j f
    , EnumerateFromTo j k x
    ) => EnumerateFromTo i k (f x)
instance {-# OVERLAPPING #-} i ~ j => EnumerateFromTo i j (Var k)
instance {-# INCOHERENT #-}
    ( EnumerateFromTo i j b
    , y ~?~ (Var j :: b)
    , k ~ If (y == Var j) (j + 1) j
    ) => EnumerateFromTo i k (y :: b)
instance i ~ j => EnumerateFromTo i j *
instance i ~ j => EnumerateFromTo i j (->)
-- https://youtu.be/FXBHY7uco0Y?t=60

debugPolyTypeOf :: EnumerateFromTo 0 k a => a -> a
debugPolyTypeOf = id

idProxy1 :: forall b proxy (f :: Symbol -> b). proxy f -> proxy f
idProxy1 = id

idProxy2 :: forall b (f :: Symbol -> b). Proxy f -> Proxy f
idProxy2 = id

idProxy3 :: forall a. Proxy ('[] :: [a]) -> Proxy ('[] :: [a])
idProxy3 = id

-- >>> import Data.Proxy
-- >>> polyTypeOf $ \x y -> x
-- forall (a :: *) (b :: *). a -> b -> a
-- >>> polyTypeOf Proxy
-- forall (a :: *) (x :: a). Proxy x
-- >>> polyTypeOf idProxy1
-- forall (a :: *) (f :: (Symbol -> a) -> *) (g :: Symbol -> a). f g -> f g
-- >>> polyTypeOf idProxy2
-- forall (a :: *) (f :: Symbol -> a). Proxy f -> Proxy f
-- >>> polyTypeOf idProxy3
-- Proxy '[] -> Proxy '[]

-- >>> import Data.Bifunctor
-- >>> import Data.Proxy
-- >>> polyTypeOf $ \x y -> x
-- forall (a :: *) (b :: *). a -> b -> a
-- >>> polyTypeOf $ let fix f = f (fix f) in fix
-- forall (a :: *). (a -> a) -> a
-- >>> polyTypeOf bimap
-- forall (a :: *) (b :: *) (c :: *) (d :: *) (f :: * -> * -> *). (a -> b) -> (c -> d) -> f a c -> f b d
-- >>> polyTypeOf elem
-- forall (a :: *) (f :: * -> *). a -> f a -> Bool
-- >>> polyTypeOf map
-- forall (a :: *) (b :: *). (a -> b) -> [a] -> [b]
-- >>> polyTypeOf 3
-- forall (a :: *). a
-- >>> polyTypeOf Proxy
-- forall (a :: *) (x :: a). Proxy x



-- instance i ~ j => EnumerateFromTo i j (->)

-- type IdentifyFromTo :: forall b. Nat -> Nat -> b -> Constraint
-- class IdentifyFromTo i j y | i y -> j
-- instance
--     ( x ~ Var @b i
-- --     , reserved ~ (b === Nat)
-- --     , TryDiscriminate reserved diff b Nat
--     , same ~ (x === y)
--     , TryUnify same x y
--     , j ~ If same (i + 1) i
--     ) => IdentifyFromTo i j (y :: b)

-- type EnumerateFromTo :: forall b. Nat -> Nat -> b -> Constraint
-- class EnumerateFromTo i j y | i y -> j
-- instance {-# OVERLAPPABLE #-}
--     ( EnumerateFromTo i j f
--     , EnumerateFromTo j k x
--     ) => EnumerateFromTo i k (f x)
-- instance {-# OVERLAPPING #-} i ~ j => EnumerateFromTo i j (Var k)
-- instance i ~ j => EnumerateFromTo i j *
-- -- instance i ~ j => EnumerateFromTo i j (->)

-- type EnumerateFromToType :: Nat -> Nat -> * -> Constraint
-- class EnumerateFromToType i j b | i b -> j
-- instance {-# OVERLAPPING #-} i ~ j => EnumerateFromToType i j *
-- instance {-# OVERLAPPING #-} i ~ j => EnumerateFromToType i j (Var k)
-- instance {-# OVERLAPPABLE #-} EnumerateFromTo i j b => EnumerateFromToType i j b

-- type IsVarApp :: * -> Bool
-- type family IsVa

-- type ShouldEnumerateType :: * -> Bool
-- type family ShouldEnumerateType b where
--     ShouldEnumerateType *        = 'False
--     ShouldEnumerateType (* -> b) = ShouldEnumerateType b
-- --     ShouldEnumerateType (Var _)  = 'False
--     ShouldEnumerateType (f x)    = 'True
--     ShouldEnumerateType b        = 'False

-- type EnumerateFromToType :: Bool -> Nat -> Nat -> * -> Constraint
-- class EnumerateFromToType s i j b | i b -> j
-- instance i ~ j => EnumerateFromToType 'False i j b
-- instance EnumerateFromTo i j b => EnumerateFromToType 'True i j b

-- instance {-# INCOHERENT #-}
--     ( IdentifyFromTo i j b
--     , s ~ ShouldEnumerateType b
--     , EnumerateFromToType s j k b
--     , IdentifyFromTo k l y
--     ) => EnumerateFromTo i l (y :: b)

data VarInfo = VarInfo
    { _varInfoId   :: Integer
    , _varInfoKind :: ReifiedType VarInfo
    } deriving (Eq)

data ReifiedType var
    = RVar var
    | RApply (ReifiedType var) (ReifiedType var)
    | RArrow
    | RStar
    | RMeta String
    deriving (Eq, Foldable)

class ReifyType (a :: k) where
    reifyType :: Proxy a -> ReifiedType VarInfo

instance ReifyType (*) where
    reifyType _ = RStar

instance ReifyType (->) where
    reifyType _ = RArrow

instance {-# OVERLAPPING #-} (KnownNat i, ReifyType k) => ReifyType (Var i :: k) where
    reifyType _ = RVar $ VarInfo (natVal @i Proxy) (reifyType $ Proxy @k)

instance {-# OVERLAPS #-} (ReifyType f, ReifyType a) => ReifyType (f a) where
    reifyType _ = RApply (reifyType $ Proxy @f) (reifyType $ Proxy @a)

instance {-# OVERLAPPABLE #-} Typeable any => ReifyType any where
    reifyType = RMeta . show . typeRepTyCon . typeRep

infixl 4 :$
data PolyType
    = Var String
    | PolyType :$ PolyType
    | Arrow
    | Star
    | Meta String
    | Forall [(String, PolyType)] PolyType

extractVars :: ReifiedType VarInfo -> [VarInfo]
extractVars = nub . collectVars where
    collectVars = uncurry (++) . foldMap (\var -> (collectVars $ _varInfoKind var, [var]))

type VarNames = [String]

defaultVarNames :: (VarNames, VarNames, VarNames)
defaultVarNames = (hks, tys, els) where
    hks = ["f", "g", "h"]
    tys = ["a", "b", "c", "d"]
    els = ["x", "y", "z"]

pickVarName :: VarNames -> (String, VarNames)
pickVarName []             = error "not enough names"
pickVarName (name : names) = (name, names)

toVarIdNames :: [VarInfo] -> [(Integer, String)]
toVarIdNames = go defaultVarNames where
    go _ [] = []
    go (hks, tys, els) (VarInfo n kind : vars) = (n, a) : go names' vars where
        (a, names') = case kind of
            RStar                      -> pickVarName tys <&> \tys' -> (hks, tys', els)
            RApply (RApply RArrow _) _ -> pickVarName hks <&> \hks' -> (hks', tys, els)
            _                          -> pickVarName els <&> \els' -> (hks, tys, els')

toFinalTypeBody :: (Integer -> String) -> ReifiedType VarInfo -> PolyType
toFinalTypeBody toVarName = go where
    go (RVar (VarInfo varId _)) = Var $ toVarName varId
    go (RApply fun arg)         = go fun :$ go arg
    go RArrow                   = Arrow
    go RStar                    = Star
    go (RMeta name)             = Meta name

toPolyType :: ReifiedType VarInfo -> PolyType
toPolyType ty0 = addForalls $ toFinalTypeBody toVarName ty0 where
    vars0 = extractVars ty0
    varIdNames = toVarIdNames vars0
    toVarName varId = fromMaybe (error "internal error") $ lookup varId varIdNames

    toBinding (VarInfo varId kind) = (toVarName varId, toFinalTypeBody toVarName kind)
    addForalls body = Forall (map toBinding vars0) body

instance Show PolyType where
    showsPrec p e = case e of
       Var name -> showParen (p > 10) $ showString name
       Meta "[]" :$ x -> showParen (p > 10) $ showString "[" . showsPrec 1 x . showString "]"
       Meta "(,)" :$ x :$ y ->
           showParen (p > 10)
               $ showString "("
               . showsPrec 1 x
               . showString ", "
               . showsPrec 1 y
               . showString ")"
       Meta name -> showParen (p > 10) $ showString name
       Arrow :$ x :$ y -> showParen (p > 2) $ showsPrec 3 x . showString " -> " . showsPrec 2 y
       Arrow -> showParen (p > 10) $ showString "(->)"
       Star -> showParen (p > 10) $ showString "*"
       f :$ x -> showParen (p > 9) $ showsPrec 9 f . showString " " . showsPrec 10 x
       Forall []    body -> showParen (p > 10) $ showsPrec 1 body
       Forall binds body ->
           showParen (p > 10)
               $ showString "forall"
               . showString (binds >>= \(name, kind) -> " (" ++ name ++ " :: " ++ show kind ++ ")")
               . showString ". "
               . showsPrec 1 body

polyTypeOf :: forall a k. (ReifyType a, EnumerateFromTo 0 k a) => a -> PolyType
polyTypeOf _ = toPolyType . reifyType $ Proxy @a

instance Eq (Var i)
instance Num (Var i)
instance Foldable (Var i)
instance Bifunctor (Var i)

-- >>> import Data.Bifunctor
-- >>> import Data.Proxy
-- >>> polyTypeOf $ \x y -> x
-- <interactive>:249:2-23: error:
--     • Reduction stack overflow; size = 201
--       When simplifying the following type: EnumerateFromTo 0 j0 (->)
--       Use -freduction-depth=0 to disable this check
--       (any upper bound you could choose might fail unpredictably with
--        minor updates to GHC, so disabling the check is recommended if
--        you're sure that type checking should terminate)
--     • In the expression: polyTypeOf $ \ x y -> x
--       In an equation for ‘it’: it = polyTypeOf $ \ x y -> x
-- >>> polyTypeOf $ let fix f = f (fix f) in fix
-- <interactive>:250:2-42: error:
--     • Reduction stack overflow; size = 201
--       When simplifying the following type: EnumerateFromTo 0 j0 (->)
--       Use -freduction-depth=0 to disable this check
--       (any upper bound you could choose might fail unpredictably with
--        minor updates to GHC, so disabling the check is recommended if
--        you're sure that type checking should terminate)
--     • In the expression: polyTypeOf $ let fix f = f (fix f) in fix
--       In an equation for ‘it’:
--           it = polyTypeOf $ let fix f = f (fix f) in fix
-- >>> polyTypeOf bimap
-- <interactive>:251:2-17: error:
--     • Reduction stack overflow; size = 201
--       When simplifying the following type: EnumerateFromTo 0 j0 (->)
--       Use -freduction-depth=0 to disable this check
--       (any upper bound you could choose might fail unpredictably with
--        minor updates to GHC, so disabling the check is recommended if
--        you're sure that type checking should terminate)
--     • In the expression: polyTypeOf bimap
--       In an equation for ‘it’: it = polyTypeOf bimap
-- >>> polyTypeOf elem
-- <interactive>:252:2-16: error:
--     • Reduction stack overflow; size = 201
--       When simplifying the following type: EnumerateFromTo 0 j0 (->)
--       Use -freduction-depth=0 to disable this check
--       (any upper bound you could choose might fail unpredictably with
--        minor updates to GHC, so disabling the check is recommended if
--        you're sure that type checking should terminate)
--     • In the expression: polyTypeOf elem
--       In an equation for ‘it’: it = polyTypeOf elem
-- >>> polyTypeOf map
-- <interactive>:253:2-15: error:
--     • Reduction stack overflow; size = 201
--       When simplifying the following type: EnumerateFromTo 0 j0 (->)
--       Use -freduction-depth=0 to disable this check
--       (any upper bound you could choose might fail unpredictably with
--        minor updates to GHC, so disabling the check is recommended if
--        you're sure that type checking should terminate)
--     • In the expression: polyTypeOf map
--       In an equation for ‘it’: it = polyTypeOf map
-- >>> polyTypeOf 3
-- <interactive>:254:2-13: error:
--     • No instance for (GHC.TypeNats.KnownNat j0)
--         arising from a use of ‘polyTypeOf’
--     • In the expression: polyTypeOf 3
--       In an equation for ‘it’: it = polyTypeOf 3
-- >>> polyTypeOf Proxy
-- <interactive>:255:2-17: error:
--     • Reduction stack overflow; size = 201
--       When simplifying the following type:
--         EnumerateFromTo 0 j0 (* -> * -> *)
--       Use -freduction-depth=0 to disable this check
--       (any upper bound you could choose might fail unpredictably with
--        minor updates to GHC, so disabling the check is recommended if
--        you're sure that type checking should terminate)
--     • In the expression: polyTypeOf Proxy
--       In an equation for ‘it’: it = polyTypeOf Proxy


-- >>> import Control.Monad
-- >>> import Control.Arrow
-- >>> import Control.Monad.IO.Class
-- >>> import Data.Bifunctor
-- >>> (\x y -> x) & Main.typeOf
-- forall (a :: *) (b :: *). a -> b -> a
-- >>> (let fix f = f (fix f) in fix) & Main.typeOf
-- forall (a :: *). (a -> a) -> a
-- >>> map & Main.typeOf
-- forall (a :: *) (b :: *). (a -> b) -> [a] -> [b]
-- >>> bimap & Main.typeOf
-- forall (a :: *) (b :: *) (c :: *) (d :: *) (f :: * -> * -> *). Bifunctor f => (a -> b) -> (c -> d) -> f a c -> f b d
-- >>> elem & Main.typeOf
-- forall (a :: *) (t :: * -> *). (Eq a, Foldable t) => a -> t a -> Bool
-- >>> 42 & Main.typeOf
-- forall (a :: *). Num a => a
-- >>> (\x -> x == 42) & Main.typeOf
-- forall (a :: *). (Eq a, Num a) => a -> Bool
-- >>> traverse & Main.typeOf
-- forall (a :: *) (f :: * -> *) (b :: *) (t :: * -> *). (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b)
-- >>> Proxy & Main.typeOf
-- forall (a :: *) (x :: a). Proxy x
-- >>> (***) & Main.typeOf
-- forall (f :: * -> * -> *) (a :: *) (b :: *) (c :: *) (d :: *). Arrow f => f a b -> f c d -> f (a, c) (b, d)
-- >>> print & Main.typeOf
-- forall (a :: *). Show a => a -> IO ()
-- >>> liftIO & Main.typeOf
-- forall (a :: *) (m :: * -> *). MonadIO m => IO a -> m a
-- >>> throwTo & Main.typeOf
-- forall (e :: *). Exception e => ThreadId -> e -> IO ()
-- >>> catches & Main.typeOf
-- forall (a :: *). IO a -> [Handler a] -> IO a
-- >>> try & Main.typeOf
-- forall (a :: *) (e :: *). Exception e => IO a -> IO (Either e a)


main = pure ()

Main.hs

{-# OPTIONS_GHC -Wall -fno-warn-missing-methods #-}

{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE DeriveFoldable           #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE FunctionalDependencies   #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}

module Main where

import           Data.Bifunctor
import           Data.Foldable
import           Data.Function
import           Data.Kind
import           Data.List
import           Data.Maybe
import           Data.Proxy
import           Data.Type.Bool
import           Data.Type.Equality
import           Data.Typeable
import           GHC.Exts           hiding (toList)
import           GHC.TypeLits

main :: IO ()
main = mempty

infix 4 ===
type (===) :: forall a b. a -> b -> Bool
type family x === y where
    x === x = 'True
    x === y = 'False

type TryUnify :: forall a b. Bool -> a -> b -> Constraint
class same ~ (x === y) => TryUnify same x y
instance {-# INCOHERENT #-} (x ~~ y, same ~ 'True) => TryUnify same x y
instance (x === y) ~ 'False => TryUnify 'False x y

-- type TryUnify :: forall a b. Bool -> a -> b -> Constraint
-- class TryUnify same x y
-- instance {-# INCOHERENT #-} same ~ 'True => TryUnify same x y
-- instance TryUnify 'False x y

type (~?~) :: forall a b. a -> b -> Constraint
type a ~?~ b = TryUnify (a === b) a b

-- class SpecializeAllAs (x :: a) (y :: b)
-- instance {-# INCOHERENT #-} x ~?~ y => SpecializeAllAs x y
-- instance (SpecializeAllAs x y, SpecializeAllAs x f) => SpecializeAllAs x (f y)

class SpecializeAllAs (x :: a) (y :: b)
instance {-# INCOHERENT #-} (SpecializeAllAs x b, x ~?~ y) => SpecializeAllAs x (y :: b)
instance (SpecializeAllAs x y, SpecializeAllAs x f) => SpecializeAllAs x (f y)

specializeAllAsInt :: SpecializeAllAs Int a => a -> a
specializeAllAsInt = id

specializeAllAsList :: SpecializeAllAs [] a => a -> a
specializeAllAsList = id

-- >>> :t specializeAllAsInt undefined
-- specializeAllAsInt undefined :: Int
-- >>> :t specializeAllAsInt map
-- specializeAllAsInt map :: (Int -> Int) -> [Int] -> [Int]
-- >>> :t specializeAllAsInt elem
-- specializeAllAsInt elem :: Foldable t => Int -> t Int -> Bool
-- >>> :t specializeAllAsList $ specializeAllAsInt elem
-- specializeAllAsList $ specializeAllAsInt elem
--   :: Int -> [Int] -> Bool
-- >>> :t specializeAllAsInt $ \x y -> x
-- specializeAllAsInt $ \x y -> x :: Int -> Int -> Int
-- >>> :t specializeAllAsInt fmap
-- specializeAllAsInt fmap
--   :: Functor f => (Int -> Int) -> f Int -> f Int
-- >>> :t specializeAllAsList fmap
-- specializeAllAsList fmap :: (a -> b) -> [a] -> [b]
-- >>> :t specializeAllAsInt "abc"
-- specializeAllAsInt "abc" :: [Char]
-- >>> :t specializeAllAsInt 3
-- specializeAllAsInt 3 :: Int




-- type Var :: forall k. Nat -> k
-- data family Var i

-- type EnumerateFromTo :: forall b. Nat -> Nat -> b -> Constraint
-- class EnumerateFromTo i j y | i y -> j
-- instance {-# INCOHERENT #-}
--     ( x ~ Var @b i
--     , same ~ (x === y)
--     , TryUnify same x y
--     , j ~ If same (i + 1) i
--     ) => EnumerateFromTo i j (y :: b)
-- instance (EnumerateFromTo i j f, EnumerateFromTo j k x) => EnumerateFromTo i k (f x)

-- infixl 4 :$
-- data ReifiedType
--     = Var Integer
--     | ReifiedType :$ ReifiedType
--     | Arrow
--     | Meta String

-- class ReifyType (a :: k) where
--     reifyType :: proxy a -> ReifiedType

-- instance {-# OVERLAPPING #-} (KnownNat i) => ReifyType (Var i) where
--     reifyType _ = Var (natVal @i Proxy)

-- instance ReifyType (->) where
--     reifyType _ = Arrow

-- instance {-# OVERLAPS #-} (ReifyType f, ReifyType a) => ReifyType (f a) where
--     reifyType _ = reifyType (Proxy @f) :$ reifyType (Proxy @a)

-- instance {-# OVERLAPPABLE #-} Typeable any => ReifyType any where
--     reifyType = Meta . show . typeRep

-- instance Show ReifiedType where
--     showsPrec p e = case e of
--        Var i           -> showParen (p > 10) . showString $ "x_" ++ show i where
--        Arrow :$ x :$ y -> showParen (p > 2) $ showsPrec 3 x . showString " -> " . showsPrec 2 y
--        Arrow           -> showParen (p > 10) $ showString "(->)"
--        f :$ x          -> showParen (p > 9) $ showsPrec 9 f . showString " " . showsPrec 10 x
--        Meta name       -> showParen (p > 10) $ showString name

-- typeOf :: forall a k. (ReifyType a, EnumerateFromTo 0 k a) => a -> ReifiedType
-- typeOf _ = reifyType $ Proxy @a

-- instance Eq (Var i)
-- instance Num (Var i)
-- instance Foldable (Var i)
-- instance Bifunctor (Var i)

-- -- >>> import Data.Bifunctor
-- -- >>> typeOf $ \x y -> x
-- -- x_0 -> x_1 -> x_0
-- -- >>> typeOf $ let fix f = f (fix f) in fix
-- -- (x_0 -> x_0) -> x_0
-- -- >>> typeOf bimap
-- -- (x_0 -> x_1) -> (x_2 -> x_3) -> x_4 x_0 x_2 -> x_4 x_1 x_3
-- -- >>> typeOf elem
-- -- x_0 -> x_1 x_0 -> Bool
-- -- >>> typeOf map
-- -- (x_0 -> x_1) -> [] x_0 -> [] x_1
-- -- >>> typeOf 3
-- -- x_0



type Var :: forall k. Nat -> k
data family Var i

-- type TypeOfArgOf :: forall b. b -> Type
-- type family TypeOfArgOf y where
--     TypeOfArgOf (_ (x :: a)) = a

-- type ArgOf :: forall b. b -> TypeOfArgOf b
-- type family ArgOf y where
--     ArgOf (_ x) = x

type ArgOf :: forall a b. b -> a
type family ArgOf y where
    ArgOf (_ x) = x

-- type CodOf :: Type -> Type
-- type family CodOf ab where
--     CodOf (a -> b) = b

-- type ArgOf :: forall a b. a -> b -> Constraint
-- class ArgOf x y | y -> x
-- instance y ~ f x => ArgOf x y

-- type TryDiscriminate :: forall a b. Bool -> a -> b -> Constraint
-- class same ~ (x === y) => TryDiscriminate same x y
-- instance {-# INCOHERENT #-} ((x === y) ~ 'False, same ~ 'False) => TryDiscriminate same x y
-- instance x ~~ y => TryDiscriminate 'True x y

type TryDiscriminate :: forall a b. Bool -> Bool -> a -> b -> Constraint
class TryDiscriminate same diff x y | same -> diff
instance {-# INCOHERENT #-} diff ~ 'True => TryDiscriminate same diff x y
instance diff ~ 'False => TryDiscriminate 'True diff x y

-- type EnumerateFromTo :: forall b. Nat -> Nat -> b -> Constraint
-- class EnumerateFromTo i j y | i y -> j
-- instance {-# INCOHERENT #-}
--     ( constrs ~ ArgOf @[Symbol] y
--     , x ~ (Var i constrs :: b)
--     , same ~ (x === y && Not (b == [Symbol]))
--     , TryUnify same (x :: b) y
--     , j ~ If same (i + 1) i
--     ) => EnumerateFromTo i j (y :: b)

type IdentifyFromTo :: forall b. Nat -> Nat -> b -> Constraint
class IdentifyFromTo i j y | i y -> j
instance
    ( constrs ~ ArgOf @[Symbol] y
    , x ~ (Var i constrs :: b)
    , reserved ~ (b === [Symbol])
    , TryDiscriminate reserved diff b [Symbol]
    , same ~ (diff && x === y)
    , TryUnify same (x :: b) y
    , j ~ If same (i + 1) i
    ) => IdentifyFromTo i j (y :: b)

type EnumerateFromTo :: forall b. Nat -> Nat -> b -> Constraint
class EnumerateFromTo i j y | i y -> j
instance {-# INCOHERENT #-}
    ( IdentifyFromTo i j b
    , IdentifyFromTo j k y
    ) => EnumerateFromTo i k (y :: b)
instance
    ( EnumerateFromTo i j f
    , EnumerateFromTo j k x
    ) => EnumerateFromTo i k (f x)

-- >>> import Data.Proxy
-- >>> import Data.Typeable
-- >>> import GHC.TypeLits
-- >>> typeRep (Proxy :: Proxy Symbol)
-- Symbol

-- >>> :set -XDataKinds
-- >>> :set -XKindSignatures
-- >>> typeRep (Proxy :: Proxy (Proxy ()))
-- Proxy * ()


-- >>> import Data.Function
-- >>> :t Proxy & Main.debugTypeOf
-- Proxy & Main.debugTypeOf :: Proxy (Var 1 constrs2)
-- >>> Proxy & Main.typeOf
-- Proxy x_1_with

type Elem :: forall a. a -> [a] -> Constraint
class x `Elem` xs where

type ElemMatch :: forall a. a -> [a] -> Constraint
type family x `ElemMatch` xs :: Constraint where
    x `ElemMatch` (x ': xs) = ()
    x `ElemMatch` (_ ': xs) = x `Elem` xs

instance (xs ~ (x' ': xs'), x ~?~ x', x `ElemMatch` xs) => x `Elem` xs

data VarInfo = VarInfo
    { _varInfoId      :: Int
    , _varInfoKind    :: ReifiedType VarInfo
    , _varInfoConstrs :: [String]
    } deriving (Show, Eq)

data ReifiedType var
    = RVar var
    | RApply (ReifiedType var) (ReifiedType var)
    | RArrow
    | RStar
    | RMeta String
    deriving (Show, Eq, Foldable)

type All :: forall a. (a -> Constraint) -> [a] -> Constraint
class All c xs where
    withElem :: Proxy (All c xs) -> (forall x. c x => Proxy x -> r) -> [r]

instance All c '[] where
    withElem _ _ = []

instance (c x, All c xs) => All c (x ': xs) where
    withElem _ f = f (Proxy @x) : withElem (Proxy @(All c xs)) f

class ReifyType (a :: k) where
    reifyType :: proxy a -> ReifiedType VarInfo

instance {-# OVERLAPPING #-} (KnownNat i, All KnownSymbol constrs, ReifyType k) =>
            ReifyType (Var i constrs :: k) where
    reifyType _ =
        RVar $ VarInfo
            (fromInteger $ natVal @i Proxy)
            (reifyType $ Proxy @k)
            (withElem (Proxy @(All KnownSymbol constrs)) symbolVal)

instance ReifyType (*) where
    reifyType _ = RStar

instance ReifyType (->) where
    reifyType _ = RArrow

instance {-# OVERLAPS #-} (ReifyType f, ReifyType x) => ReifyType (f x) where
    reifyType _ = RApply (reifyType $ Proxy @f) (reifyType $ Proxy @x)

instance {-# OVERLAPPABLE #-} Typeable any => ReifyType any where
    -- It's safe to use 'typeRepTyCon' here, because the @(->)@ and @f x@ cases are handled above.
    reifyType = RMeta . show . typeRepTyCon . typeRep

data FinalType
    = Var String
    | FinalType :$ FinalType
    | Star
    | Arrow
    | Meta String
    | Forall [(String, FinalType)] FinalType
    | Constraints [String] FinalType

instance Show FinalType where
    showsPrec p = \case
       Var name -> showParen (p > 10) $ showString name
       Star -> showParen (p > 10) $ showString "*"
       Meta "[]" :$ x -> showParen (p > 10) $ showString "[" . showsPrec 1 x . showString "]"
       Meta "(,)" :$ x :$ y ->
           showParen (p > 10)
               $ showString "("
               . showsPrec 1 x
               . showString ", "
               . showsPrec 1 y
               . showString ")"
       Meta name -> showParen (p > 10) $ showString name
       Arrow :$ x :$ y -> showParen (p > 2) $ showsPrec 3 x . showString " -> " . showsPrec 2 y
       Arrow -> showParen (p > 10) $ showString "(->)"
       f :$ x -> showParen (p > 9) $ showsPrec 9 f . showString " " . showsPrec 10 x
       Forall binds body ->
           showParen (p > 10)
               $ showString "forall"
               . showString (binds >>= \(name, kind) -> " (" ++ name ++ " :: " ++ show kind ++ ")")
               . showString ". "
               . showsPrec 1 body
       Constraints constrs body ->
           showParen (p > 10)
               $ showString constrsString
               . showsPrec 1 body
         where
           constrsString = case constrs of
               []       -> ""
               [constr] -> constr ++ " => "
               _        -> "(" ++ intercalate ", " constrs ++ ") => "

extractVars :: ReifiedType VarInfo -> [VarInfo]
extractVars
    = check
    . map the
    . groupBy ((==) `on` _varInfoId)
    . sortOn _varInfoId
    . collectVars
  where
    collectVars = concatMap (\var -> var : collectVars (_varInfoKind var)) . toList

    err vars = error $ "bad indices in " ++ show vars
    check vars =
        zipWith
            (\i var@(VarInfo varId _ _) -> if i == varId then var else err vars)
            [0..]
            vars

toFinalType :: ReifiedType VarInfo -> FinalType
toFinalType ty0 = addForalls . addConstrs $ process ty0 where
    vars0 = extractVars ty0
    varNames = go ["f", "g", "h"] ["a", "b", "c", "d", "e"] ["x", "y", "z", "s", "t"] vars0 where
        go _ _ _ [] = []
        go hks ~(ty : tys) els (VarInfo n RStar                        _ : vars) =
            (n, ty) : go hks tys els vars
        go ~(hk : hks) tys els (VarInfo n (RApply (RApply RArrow _) _) _ : vars) =
            (n, hk) : go hks tys els vars
        go hks tys ~(el : els) (VarInfo n _                            _ : vars) =
            (n, el) : go hks tys els vars

    addVarConstr varId constr = constr ++ " " ++ toVarName varId
    addVarConstrs (VarInfo varId _ constrs) = map (addVarConstr varId) constrs
    addConstrs = Constraints $ concatMap addVarConstrs vars0
    toBinding (VarInfo varId kind _) = (toVarName varId, process kind)
    addForalls body = Forall (map toBinding vars0) body

    process (RVar (VarInfo varId _ _)) = Var $ toVarName varId
    process (RApply fun arg)           = process fun :$ process arg
    process RArrow                     = Arrow
    process RStar                      = Star
    process (RMeta name)               = Meta name

    toVarName varId = fromMaybe (error "lacking variable names") $ lookup varId varNames

typeOf :: forall a k. (EnumerateFromTo 0 k a, ReifyType a, SpecializeAllAs ('[] :: [Symbol]) a) => a -> FinalType
typeOf _ = toFinalType . reifyType $ Proxy @a

debugTypeOf :: forall a k. (EnumerateFromTo 0 k a) => a -> a
debugTypeOf = id

instance "Eq"        `Elem` constrs => Eq        (Var i constrs)
instance "Num"       `Elem` constrs => Num       (Var i constrs)
instance "Foldable"  `Elem` constrs => Foldable  (Var i constrs)
instance "Bifunctor" `Elem` constrs => Bifunctor (Var i constrs)

-- >>> import Data.Function
-- >>> import Data.Bifunctor
-- >>> bimap & Main.typeOf
-- forall (a :: *) (b :: *) (c :: *) (d :: *) (f :: * -> * -> *). Bifunctor f => (a -> b) -> (c -> d) -> f a c -> f b d
-- >>> elem & Main.typeOf
-- forall (a :: *) (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool

-- >>> import Data.Bifunctor
-- >>> (\x y -> x) & Main.typeOf
-- forall (a :: *) (b :: *). a -> b -> a
-- >>> (let fix f = f (fix f) in fix) & Main.typeOf
-- forall (a :: *). (a -> a) -> a
-- >>> map & Main.typeOf
-- forall (a :: *) (b :: *). (a -> b) -> [a] -> [b]
-- >>> bimap & Main.typeOf
-- forall (a :: *) (b :: *) (c :: *) (d :: *) (f :: * -> * -> *). Bifunctor f => (a -> b) -> (c -> d) -> f a c -> f b d
-- >>> elem & Main.typeOf
-- forall (a :: *) (f :: * -> *). (Eq a, Foldable f) => a -> f a -> Bool
-- >>> 3 & Main.typeOf
-- forall (a :: *). Num a => a
-- >>> fst & Main.typeOf
-- forall (a :: *) (b :: *). (a, b) -> a
-- >>> Proxy & Main.typeOf
-- forall (a :: *) (x :: a). Proxy x





{-

-- type MatchSpecializeAllAs :: forall a b. a -> b -> Constraint
-- type family MatchSpecializeAllAs x y where
--     MatchSpecializeAllAs x x     = ()
--     MatchSpecializeAllAs x (f y) = (SpecializeAllAs x f, SpecializeAllAs x y)
--     MatchSpecializeAllAs x y     = ()

-- type SpecializeAllAs :: forall a b. a -> b -> Constraint
-- class SpecializeAllAs x y
-- instance (x ~?~ y, MatchSpecializeAllAs x y) => SpecializeAllAs x y




type family SpecializesAs a b (x :: a) (y :: b) where
    SpecializesAs a a x x = 'True
    SpecializesAs a b x y = 'False

class SpecializesAs a b x y ~ is => IsSpecializable is (x :: a) (y :: b)
instance {-# INCOHERENT #-} (x ~~ y, is ~ 'True) => IsSpecializable is (x :: a) (y :: b)
instance SpecializesAs a b x y ~ 'False => IsSpecializable 'False (x :: a) (y :: b)

type TrySpecializeAs (x :: a) (y :: b) = IsSpecializable (SpecializesAs a b x y) x y

class SpecializeAllAs (x :: a) (y :: b)
instance {-# INCOHERENT #-} TrySpecializeAs x y => SpecializeAllAs x y
instance (SpecializeAllAs x y, SpecializeAllAs x f) => SpecializeAllAs x (f y)

specializeAllAsInt :: SpecializeAllAs Int a => a -> a
specializeAllAsInt = id

specializeAllAsList :: SpecializeAllAs [] a => a -> a
specializeAllAsList = id

-- >>> :t specializeAllAsInt undefined
-- specializeAllAsInt undefined :: Int
-- >>> :t specializeAllAsInt map
-- specializeAllAsInt map :: (Int -> Int) -> [Int] -> [Int]
-- >>> :t specializeAllAsInt elem
-- specializeAllAsInt elem :: Foldable t => Int -> t Int -> Bool
-- >>> :t specializeAllAsList $ specializeAllAsInt elem
-- specializeAllAsList $ specializeAllAsInt elem
--   :: Int -> [Int] -> Bool
-- >>> :t specializeAllAsInt (\x y -> x)
-- specializeAllAsInt (\x y -> x) :: Int -> Int -> Int
-- >>> :t specializeAllAsInt fmap
-- specializeAllAsInt fmap
--   :: Functor f => (Int -> Int) -> f Int -> f Int
-- >>> :t specializeAllAsList fmap
-- specializeAllAsList fmap :: (a -> b) -> [a] -> [b]
-- >>> :t specializeAllAsInt "abc"
-- specializeAllAsInt "abc" :: [Char]
-- >>> :t specializeAllAsInt 3
-- specializeAllAsInt 3 :: Int

data family Var (i :: Nat) :: k

class EnumerateWith (i :: Nat) (j :: Nat) (y :: b) | i y -> j
instance {-# INCOHERENT #-}
    ( x ~ Var i
    , is ~ SpecializesAs b b x y
    , IsSpecializable is x y
    , j ~ If is (i + 1) i
    ) => EnumerateWith i j (y :: b)
instance (EnumerateWith i j f, EnumerateWith j k x) => EnumerateWith i k (f x)

infixl 4 :$
data ReifiedType
    = Var Integer
    | ReifiedType :$ ReifiedType
    | Arrow
    | Meta String

class ReifyType (a :: k) where
    reifyType :: proxy a -> ReifiedType

instance {-# OVERLAPPING #-} (KnownNat i) => ReifyType (Var i) where
    reifyType _ = Var (natVal @i Proxy)

instance ReifyType (->) where
    reifyType _ = Arrow

instance {-# OVERLAPS #-} (ReifyType f, ReifyType a) => ReifyType (f a) where
    reifyType _ = reifyType (Proxy @f) :$ reifyType (Proxy @a)

instance {-# OVERLAPPABLE #-} Typeable any => ReifyType any where
    reifyType = Meta . show . typeRep

instance Show ReifiedType where
    showsPrec p e = case e of
       Var i           -> showParen (p > 10) . showString $ "x_" ++ show i where
       Arrow :$ x :$ y -> showParen (p > 2) $ showsPrec 3 x . showString " -> " . showsPrec 2 y
       Arrow           -> showParen (p > 10) $ showString "(->)"
       f :$ x          -> showParen (p > 9) $ showsPrec 9 f . showString " " . showsPrec 10 x
       Meta name       -> showParen (p > 10) $ showString name

reifyTypeOf :: forall a k. (ReifyType a, EnumerateWith 0 k a) => a -> ReifiedType
reifyTypeOf _ = reifyType $ Proxy @a

instance Eq (Var i)
instance Num (Var i)
instance Foldable (Var i)
instance Bifunctor (Var i)

-- >>> reifyTypeOf $ \x y -> x
-- x_0 -> x_1 -> x_0
-- >>> reifyTypeOf $ let fix f = f (fix f) in fix
-- (x_0 -> x_0) -> x_0
-- >>> reifyTypeOf bimap
-- (x_0 -> x_1) -> (x_2 -> x_3) -> x_4 x_0 x_2 -> x_4 x_1 x_3
-- >>> reifyTypeOf elem
-- x_0 -> x_1 x_0 -> Bool
-- >>> reifyTypeOf map
-- (x_0 -> x_1) -> [] x_0 -> [] x_1
-- >>> reifyTypeOf 3
-- x_0

class (x :: a) `Elem` (xs :: [a])
type family x `ElemMatch` xs :: Constraint where
    x `ElemMatch` (x ': xs) = ()
    x `ElemMatch` (_ ': xs) = x `Elem` xs
instance (xs ~ (x' ': xs'), TrySpecializeAs x x', x `ElemMatch` xs) => x `Elem` xs

specializeAsEmptyList :: SpecializeAllAs ('[] :: [Symbol]) a => a -> a
specializeAsEmptyList = id

xsHasA :: "a" `Elem` xs => Proxy xs
xsHasA = Proxy

xsHasB :: "b" `Elem` xs => Proxy xs
xsHasB = Proxy

-- >>> :t xsHasA
-- xsHasA :: Proxy ("a" : xs')
-- >>> :t xsHasB
-- xsHasB :: Proxy ("b" : xs')
-- >>> :t [xsHasA, xsHasB]
-- [xsHasA, xsHasB] :: [Proxy ("a" : "b" : xs')]
-- >>> :t let xs = [xsHasB, xsHasA] in specializeAsEmptyList xs
-- let xs = [xsHasB, xsHasA] in specializeAsEmptyList xs
--   :: [Proxy '["b", "a"]]
-}

-- >>> :kind Proxy
-- Proxy :: k -> *

-- pr :: Proxy @(*) ()
-- pr = Proxy

-- >>> :set -XTypeApplications
-- >>> :set -XTypeOperators
-- >>> import Data.Proxy
-- >>> import Data.Typeable
-- >>> typeRep (Proxy :: Proxy (Proxy ()))
-- Proxy * ()
-- >>> (Proxy :: Proxy @(*) ())
-- <interactive>:77:12-24: error:
--     • Cannot apply function of kind ‘k0 -> *’
--       to visible kind argument ‘(*)’
--     • In an expression type signature: Proxy @(*) ()
--       In the expression: (Proxy :: Proxy @(*) ())
--       In an equation for ‘it’: it = (Proxy :: Proxy @(*) ())

Super.hs

{-# OPTIONS_GHC -Wall -fno-warn-missing-methods #-}

{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE DeriveFoldable           #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE FunctionalDependencies   #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE QuantifiedConstraints    #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE UndecidableSuperClasses  #-}

module Super where

import           Control.Arrow               hiding (first)
import           Control.Category (Category)
import           Control.Exception
import           Control.Monad.IO.Class
import           Data.Bifunctor
import           Data.Functor
import           Data.Kind
import           Data.List
import           Data.Maybe
import           Data.Proxy
import           Data.Type.Bool
import           Data.Type.Equality
import           Data.Typeable
import           GHC.TypeLits

main :: IO ()
main = mempty

infix 4 ===
type (===) :: forall a b. a -> b -> Bool
type family x === y where
    x === x = 'True
    x === y = 'False

type TryUnify :: forall a b. Bool -> a -> b -> Constraint
class same ~ (x === y) => TryUnify same x y
instance {-# INCOHERENT #-} (x ~~ y, same ~ 'True) => TryUnify same x y
instance (x === y) ~ 'False => TryUnify 'False x y

type (~?~) :: forall a b. a -> b -> Constraint
type a ~?~ b = TryUnify (a === b) a b

-- type TryUnify :: forall a b. Bool -> a -> b -> Constraint
-- class TryUnify same x y
-- instance {-# INCOHERENT #-} same ~ 'True => TryUnify same x y
-- instance TryUnify 'False x y

-- class SpecializeAllAs (x :: a) (y :: b)
-- instance {-# INCOHERENT #-} x ~?~ y => SpecializeAllAs x y
-- instance (SpecializeAllAs x y, SpecializeAllAs x f) => SpecializeAllAs x (f y)

class SpecializeAllAs (x :: a) (y :: b)
instance {-# INCOHERENT #-} (SpecializeAllAs x b, x ~?~ y) => SpecializeAllAs x (y :: b)
instance (SpecializeAllAs x y, SpecializeAllAs x f) => SpecializeAllAs x (f y)

specializeAllAsInt :: SpecializeAllAs Int a => a -> a
specializeAllAsInt = id

specializeAllAsList :: SpecializeAllAs [] a => a -> a
specializeAllAsList = id

-- >>> :t specializeAllAsInt undefined
-- specializeAllAsInt undefined :: Int
-- >>> :t specializeAllAsInt map
-- specializeAllAsInt map :: (Int -> Int) -> [Int] -> [Int]
-- >>> :t specializeAllAsInt elem
-- specializeAllAsInt elem :: Foldable t => Int -> t Int -> Bool
-- >>> :t specializeAllAsList $ specializeAllAsInt elem
-- specializeAllAsList $ specializeAllAsInt elem
--   :: Int -> [Int] -> Bool
-- >>> :t specializeAllAsInt $ \x y -> x
-- specializeAllAsInt $ \x y -> x :: Int -> Int -> Int
-- >>> :t specializeAllAsInt fmap
-- specializeAllAsInt fmap
--   :: Functor f => (Int -> Int) -> f Int -> f Int
-- >>> :t specializeAllAsList fmap
-- specializeAllAsList fmap :: (a -> b) -> [a] -> [b]
-- >>> :t specializeAllAsInt "abc"
-- specializeAllAsInt "abc" :: [Char]
-- >>> :t specializeAllAsInt 3
-- specializeAllAsInt 3 :: Int




-- type Var :: forall k. Nat -> k
-- data family Var i

-- type EnumerateFromTo :: forall b. Nat -> Nat -> b -> Constraint
-- class EnumerateFromTo i j y | i y -> j
-- instance {-# INCOHERENT #-}
--     ( x ~ Var @b i
--     , same ~ (x === y)
--     , TryUnify same x y
--     , j ~ If same (i + 1) i
--     ) => EnumerateFromTo i j (y :: b)
-- instance (EnumerateFromTo i j f, EnumerateFromTo j k x) => EnumerateFromTo i k (f x)

-- infixl 4 :$
-- data ReifiedType
--     = Var Integer
--     | ReifiedType :$ ReifiedType
--     | Arrow
--     | Meta String

-- class ReifyType (a :: k) where
--     reifyType :: proxy a -> ReifiedType

-- instance {-# OVERLAPPING #-} (KnownNat i) => ReifyType (Var i) where
--     reifyType _ = Var (natVal @i Proxy)

-- instance ReifyType (->) where
--     reifyType _ = Arrow

-- instance {-# OVERLAPS #-} (ReifyType f, ReifyType a) => ReifyType (f a) where
--     reifyType _ = reifyType (Proxy @f) :$ reifyType (Proxy @a)

-- instance {-# OVERLAPPABLE #-} Typeable any => ReifyType any where
--     reifyType = Meta . show . typeRep

-- instance Show ReifiedType where
--     showsPrec p e = case e of
--        Var i           -> showParen (p > 10) . showString $ "x_" ++ show i where
--        Arrow :$ x :$ y -> showParen (p > 2) $ showsPrec 3 x . showString " -> " . showsPrec 2 y
--        Arrow           -> showParen (p > 10) $ showString "(->)"
--        f :$ x          -> showParen (p > 9) $ showsPrec 9 f . showString " " . showsPrec 10 x
--        Meta name       -> showParen (p > 10) $ showString name

-- typeOf :: forall a k. (ReifyType a, EnumerateFromTo 0 k a) => a -> ReifiedType
-- typeOf _ = reifyType $ Proxy @a

-- instance Eq (Var i)
-- instance Num (Var i)
-- instance Foldable (Var i)
-- instance Bifunctor (Var i)

-- -- >>> import Data.Bifunctor
-- -- >>> typeOf $ \x y -> x
-- -- x_0 -> x_1 -> x_0
-- -- >>> typeOf $ let fix f = f (fix f) in fix
-- -- (x_0 -> x_0) -> x_0
-- -- >>> typeOf bimap
-- -- (x_0 -> x_1) -> (x_2 -> x_3) -> x_4 x_0 x_2 -> x_4 x_1 x_3
-- -- >>> typeOf elem
-- -- x_0 -> x_1 x_0 -> Bool
-- -- >>> typeOf map
-- -- (x_0 -> x_1) -> [] x_0 -> [] x_1
-- -- >>> typeOf 3
-- -- x_0



type Var :: forall k. Nat -> k
data family Var i

-- type TypeOfArgOf :: forall b. b -> Type
-- type family TypeOfArgOf y where
--     TypeOfArgOf (_ (x :: a)) = a

-- type ArgOf :: forall b. b -> TypeOfArgOf b
-- type family ArgOf y where
--     ArgOf (_ x) = x

type ArgOf :: forall a b. b -> a
type family ArgOf y where
    ArgOf (_ x) = x

type Arg2Of :: forall a c. c -> a
type family Arg2Of z where
    Arg2Of (_ x _) = x

-- type CodOf :: Type -> Type
-- type family CodOf ab where
--     CodOf (a -> b) = b

-- type ArgOf :: forall a b. a -> b -> Constraint
-- class ArgOf x y | y -> x
-- instance y ~ f x => ArgOf x y

-- type TryDiscriminate :: forall a b. Bool -> a -> b -> Constraint
-- class same ~ (x === y) => TryDiscriminate same x y
-- instance {-# INCOHERENT #-} ((x === y) ~ 'False, same ~ 'False) => TryDiscriminate same x y
-- instance x ~~ y => TryDiscriminate 'True x y

-- type EnumerateFromTo :: forall b. Nat -> Nat -> b -> Constraint
-- class EnumerateFromTo i j y | i y -> j
-- instance {-# INCOHERENT #-}
--     ( constrs ~ ArgOf @[Symbol] y
--     , x ~ (Var i constrs :: b)
--     , same ~ (x === y && Not (b == [Symbol]))
--     , TryUnify same (x :: b) y
--     , j ~ If same (i + 1) i
--     ) => EnumerateFromTo i j (y :: b)

type TryDiscriminate :: forall a b. Bool -> Bool -> a -> b -> Constraint
class TryDiscriminate same diff x y | same -> diff
instance {-# INCOHERENT #-} diff ~ 'True => TryDiscriminate same diff x y
instance diff ~ 'False => TryDiscriminate 'True diff x y

type IdentifyFromTo :: forall b. Nat -> Nat -> b -> Constraint
class IdentifyFromTo i j y | i y -> j
instance
    ( super ~ ArgOf @[Symbol] y
    , constrs ~ Arg2Of @[Symbol] y
    , x ~ (Var i constrs super :: b)
    , reserved ~ (b === [Symbol])
    , TryDiscriminate reserved diff b [Symbol]
    , same ~ (diff && x === y)
    , TryUnify same (x :: b) y
    , j ~ If same (i + 1) i
    ) => IdentifyFromTo i j (y :: b)

type EnumerateFromTo :: forall b. Nat -> Nat -> b -> Constraint
class EnumerateFromTo i j y | i y -> j
instance {-# INCOHERENT #-}
    ( IdentifyFromTo i j b
    , IdentifyFromTo j k y
    ) => EnumerateFromTo i k (y :: b)
instance
    ( EnumerateFromTo i j f
    , EnumerateFromTo j k x
    ) => EnumerateFromTo i k (f x)

type Elem :: forall a. a -> [a] -> Constraint
class x `Elem` xs where

type ElemMatch :: forall a. a -> [a] -> Constraint
type family x `ElemMatch` xs :: Constraint where
    x `ElemMatch` (x ': xs) = ()
    x `ElemMatch` (_ ': xs) = x `Elem` xs

instance (xs ~ (x' ': xs'), x ~?~ x', x `ElemMatch` xs) => x `Elem` xs

data VarInfo = VarInfo
    { _varInfoId      :: Integer
    , _varInfoKind    :: ReifiedType VarInfo
    , _varInfoConstrs :: [String]
    , _varInfoSuper   :: [String]
    } deriving (Show, Eq)

data ReifiedType var
    = RVar var
    | RApply (ReifiedType var) (ReifiedType var)
    | RArrow
    | RStar
    | RMeta String
    deriving (Show, Eq, Foldable)

type All :: forall a. (a -> Constraint) -> [a] -> Constraint
class All c xs where
    withElem :: Proxy (All c xs) -> (forall x. c x => Proxy x -> r) -> [r]

instance All c '[] where
    withElem _ _ = []

instance (c x, All c xs) => All c (x ': xs) where
    withElem _ f = f (Proxy @x) : withElem (Proxy @(All c xs)) f

class ReifyType (a :: k) where
    reifyType :: proxy a -> ReifiedType VarInfo

instance {-# OVERLAPPING #-}
    ( KnownNat i
    , All KnownSymbol constrs
    , All KnownSymbol super
    , ReifyType k
    ) => ReifyType (Var i constrs super :: k) where
    reifyType _ =
        RVar $ VarInfo
            (natVal @i Proxy)
            (reifyType $ Proxy @k)
            (withElem (Proxy @(All KnownSymbol constrs)) symbolVal)
            (withElem (Proxy @(All KnownSymbol super)) symbolVal)

instance ReifyType (*) where
    reifyType _ = RStar

instance ReifyType (->) where
    reifyType _ = RArrow

instance {-# OVERLAPS #-} (ReifyType f, ReifyType x) => ReifyType (f x) where
    reifyType _ = RApply (reifyType $ Proxy @f) (reifyType $ Proxy @x)

instance {-# OVERLAPPABLE #-} Typeable any => ReifyType any where
    -- It's safe to use 'typeRepTyCon' here, because the @(->)@ and @f x@ cases are handled above.
    reifyType = RMeta . show . typeRepTyCon . typeRep

data FinalType
    = Var String
    | FinalType :$ FinalType
    | Star
    | Arrow
    | Meta String
    | Forall [(String, FinalType)] FinalType
    | Constraints [String] FinalType

instance Show FinalType where
    showsPrec p = \case
       Var name -> showParen (p > 10) $ showString name
       Star -> showParen (p > 10) $ showString "*"
       Meta "[]" :$ x -> showParen (p > 10) $ showString "[" . showsPrec 1 x . showString "]"
       Meta "(,)" :$ x :$ y ->
           showParen (p > 10)
               $ showString "("
               . showsPrec 1 x
               . showString ", "
               . showsPrec 1 y
               . showString ")"
       Meta name -> showParen (p > 10) $ showString name
       Arrow :$ x :$ y -> showParen (p > 2) $ showsPrec 3 x . showString " -> " . showsPrec 2 y
       Arrow -> showParen (p > 10) $ showString "(->)"
       f :$ x -> showParen (p > 9) $ showsPrec 9 f . showString " " . showsPrec 10 x
       Forall binds body ->
           showParen (p > 10)
               $ showString "forall"
               . showString (binds >>= \(name, kind) -> " (" ++ name ++ " :: " ++ show kind ++ ")")
               . showString ". "
               . showsPrec 1 body
       Constraints constrs body ->
           showParen (p > 10)
               $ showString constrsString
               . showsPrec 1 body
         where
           constrsString = case constrs of
               []       -> ""
               [constr] -> constr ++ " => "
               _        -> "(" ++ intercalate ", " constrs ++ ") => "

extractVars :: ReifiedType VarInfo -> [VarInfo]
extractVars = nub . collectVars where
    collectVars = uncurry (++) . foldMap (\var -> (collectVars $ _varInfoKind var, [var]))

type VarNames = ([([String], [String])], [String])

defaultVarNames :: (VarNames, VarNames, VarNames)
defaultVarNames = (hks, tys, els) where
    hks =
        ( [ (["Monad"], ["m", "n"])
          , (["Foldable", "Traversable"], ["t", "s"])
          ]
        , ["f", "g", "h"]
        )
    tys =
        ( [ (["Exception"], ["e", "e'"])
          ]
        , ["a", "b", "c", "d"]
        )
    els =
        ( []
        , ["x", "y", "z"]
        )

pickVarName :: [String] -> VarNames -> (String, VarNames)
pickVarName constrs (specs0, gen) = go specs0 where
    splitNames []             = error "not enough names"
    splitNames (name : names) = (name, names)

    go [] = (,) [] <$> splitNames gen
    go ((spec, names) : specs)
        | null (spec `intersect` constrs) = first ((spec, names) :) <$> go specs
        | otherwise                       =
            (\names' -> ((spec, names') : specs, gen)) <$> splitNames names

toVarIdNames :: [VarInfo] -> [(Integer, String)]
toVarIdNames = go defaultVarNames where
    go _ [] = []
    go (hks, tys, els) (VarInfo n kind constrs _ : vars) = (n, a) : go names' vars where
        (a, names') = case kind of
            RStar                      -> pickVarName constrs tys <&> \tys' -> (hks, tys', els)
            RApply (RApply RArrow _) _ -> pickVarName constrs hks <&> \hks' -> (hks', tys, els)
            _                          -> pickVarName constrs els <&> \els' -> (hks, tys, els')

toFinalTypeBody :: (Integer -> String) -> ReifiedType VarInfo -> FinalType
toFinalTypeBody toVarName = go where
    go (RVar (VarInfo varId _ _ _)) = Var $ toVarName varId
    go (RApply fun arg)             = go fun :$ go arg
    go RArrow                       = Arrow
    go RStar                        = Star
    go (RMeta name)                 = Meta name

toFinalType :: ReifiedType VarInfo -> FinalType
toFinalType ty0 = addForalls . addConstrs $ toFinalTypeBody toVarName ty0 where
    vars0 = extractVars ty0
    varIdNames = toVarIdNames vars0
    toVarName varId = fromMaybe (error "internal error") $ lookup varId varIdNames

    addVarConstr varId constr = constr ++ " " ++ toVarName varId
    addVarConstrs (VarInfo varId _ constrs super) = map (addVarConstr varId) $ constrs \\ super
    addConstrs = Constraints $ concatMap addVarConstrs vars0
    toBinding (VarInfo varId kind _ _) = (toVarName varId, toFinalTypeBody toVarName kind)
    addForalls body = Forall (map toBinding vars0) body

class    (c, c => d) => c `Seq` d
instance (c, c => d) => c `Seq` d

polyTypeOf
    :: forall a k.
       ( EnumerateFromTo 0 k a
       , ReifyType a `Seq` SpecializeAllAs ('[] :: [Symbol]) a
       )
    => a -> FinalType
polyTypeOf _ = toFinalType . reifyType $ Proxy @a

debugPolyTypeOf :: EnumerateFromTo 0 k a => a -> a
debugPolyTypeOf = id

instance "Show"      `Elem` constrs => Show      (Var i constrs super)
instance "Eq"        `Elem` constrs => Eq        (Var i constrs super)
instance "Num"       `Elem` constrs => Num       (Var i constrs super)
instance "Functor"   `Elem` constrs => Functor   (Var i constrs super)
instance "Foldable"  `Elem` constrs => Foldable  (Var i constrs super)
instance "Bifunctor" `Elem` constrs => Bifunctor (Var i constrs super)
instance "Category"  `Elem` constrs => Category  (Var i constrs super)

-- -- "Class 'KnownNat' does not support used-defined instances"
-- instance "KnownNat" `Elem` constrs => KnownNat (Var i constrs super)

instance
    ( KnownNat i, Typeable constrs, Typeable super
    , Show (Var i constrs super)
    , "Show"  `Elem` super
    , "Exception" `Elem` constrs
    ) => Exception (Var i constrs super)
instance
    ( Functor (Var i constrs super)
    , "Functor"  `Elem` super
    , "Applicative" `Elem` constrs
    ) => Applicative (Var i constrs super)
instance
    ( Applicative (Var i constrs super)
    , "Applicative" `Elem` super
    , "Monad" `Elem` constrs
    ) => Monad (Var i constrs super)
instance
    ( Monad (Var i constrs super)
    , "Monad" `Elem` super
    , "MonadIO" `Elem` constrs
    ) => MonadIO (Var i constrs super)
instance
    ( Functor  (Var i constrs super)
    , Foldable (Var i constrs super)
    , "Functor"  `Elem` super
    , "Foldable" `Elem` super
    , "Traversable" `Elem` constrs
    ) => Traversable (Var i constrs super)
instance
    ( Category (Var i constrs super :: * -> * -> *)
    , "Category" `Elem` super
    , "Arrow" `Elem` constrs
    ) => Arrow (Var i constrs super)


-- >>> typeOf 'a'
-- Char
-- >>> typeOf (&&)
-- Bool -> Bool -> Bool
-- >>> typeOf id
-- <interactive>:1617:2-10: error:
--     • No instance for (Typeable a0) arising from a use of ‘typeOf’
--     • In the expression: typeOf id
--       In an equation for ‘it’: it = typeOf id

-- >>> polyTypeOf id
-- forall (a :: *). a -> a
-- >>> polyTypeOf (!!)
-- forall (a :: *). [a] -> Int -> a
-- >>> polyTypeOf $ \x -> x == 42
-- forall (a :: *). (Eq a, Num a) => a -> Bool
-- >>> polyTypeOf traverse
-- forall (a :: *) (f :: * -> *) (b :: *) (t :: * -> *). (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b)
-- >>> polyTypeOf Proxy
-- forall (a :: *) (x :: a). Proxy x

-- >>> import Control.Monad
-- >>> import Control.Arrow
-- >>> import Control.Monad.IO.Class
-- >>> import Data.Bifunctor
-- >>> (\x y -> x) & polyTypeOf
-- forall (a :: *) (b :: *). a -> b -> a
-- >>> (let fix f = f (fix f) in fix) & polyTypeOf
-- forall (a :: *). (a -> a) -> a
-- >>> map & polyTypeOf
-- forall (a :: *) (b :: *). (a -> b) -> [a] -> [b]
-- >>> bimap & polyTypeOf
-- forall (a :: *) (b :: *) (c :: *) (d :: *) (f :: * -> * -> *). Bifunctor f => (a -> b) -> (c -> d) -> f a c -> f b d
-- >>> elem & polyTypeOf
-- forall (a :: *) (t :: * -> *). (Eq a, Foldable t) => a -> t a -> Bool
-- >>> 42 & polyTypeOf
-- forall (a :: *). Num a => a
-- >>> (\x -> x == 42) & polyTypeOf
-- forall (a :: *). (Eq a, Num a) => a -> Bool
-- >>> traverse & polyTypeOf
-- forall (a :: *) (f :: * -> *) (b :: *) (t :: * -> *). (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b)
-- >>> Proxy & polyTypeOf
-- forall (a :: *) (x :: a). Proxy x
-- >>> (***) & polyTypeOf
-- forall (f :: * -> * -> *) (a :: *) (b :: *) (c :: *) (d :: *). Arrow f => f a b -> f c d -> f (a, c) (b, d)
-- >>> print & polyTypeOf
-- forall (a :: *). Show a => a -> IO ()
-- >>> liftIO & polyTypeOf
-- forall (a :: *) (m :: * -> *). MonadIO m => IO a -> m a
-- >>> throwTo & polyTypeOf
-- forall (e :: *). Exception e => ThreadId -> e -> IO ()
-- >>> catches & polyTypeOf
-- forall (a :: *). IO a -> [Handler a] -> IO a
-- >>> try & polyTypeOf
-- forall (a :: *) (e :: *). Exception e => IO a -> IO (Either e a)

-- Whoops
-- >>> typeRep & polyTypeOf
-- forall (a :: *) (f :: a -> *) (x :: a). f x -> SomeTypeRep

-- Whoops
-- >>> import Control.Exception
-- >>> mask & polyTypeOf
-- <interactive>:1073:2-5: error:
--     • Couldn't match expected type ‘Var 0 '[] '[]’
--                   with actual type ‘((forall a. IO a -> IO a) -> IO b0) -> IO b0’
--     • In the first argument of ‘(&)’, namely ‘mask’
--       In the expression: mask & polyTypeOf
--       In an equation for ‘it’: it = mask & polyTypeOf

TrySpecializeAs.hs

{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

import           Data.Bifunctor
import           Data.Kind
import           Data.Proxy
import           Data.Type.Bool
import           Data.Typeable
import           GHC.TypeLits

import           Unsafe.Coerce

type family SpecializesAs a b (x :: a) (y :: b) where
    SpecializesAs a a x x = 'True
    SpecializesAs a b x y = 'False

class SpecializesAs a b x y ~ is => IsSpecializable is (x :: a) (y :: b)
instance {-# INCOHERENT #-} (x ~ y, is ~ 'True) => IsSpecializable is (x :: a) (y :: a)
instance SpecializesAs a b x y ~ 'False => IsSpecializable 'False (x :: a) (y :: b)

type TrySpecializeAs (x :: a) (y :: b) = IsSpecializable (SpecializesAs a b x y) x y

class SpecializeAllAs (x :: a) (y :: b)
instance {-# INCOHERENT #-} TrySpecializeAs x y => SpecializeAllAs x y
instance (SpecializeAllAs x y, SpecializeAllAs x f) => SpecializeAllAs x (f y)

specializeAllAsInt :: SpecializeAllAs Int a => a -> a
specializeAllAsInt = id

specializeAllAsList :: SpecializeAllAs [] a => a -> a
specializeAllAsList = id

-- >>> :t specializeAllAsInt undefined
-- specializeAllAsInt undefined :: Int
-- >>> :t specializeAllAsInt map
-- specializeAllAsInt map :: (Int -> Int) -> [Int] -> [Int]
-- >>> :t specializeAllAsInt elem
-- specializeAllAsInt elem :: Foldable t => Int -> t Int -> Bool
-- >>> :t specializeAllAsList $ specializeAllAsInt elem
-- specializeAllAsList $ specializeAllAsInt elem
--   :: Int -> [Int] -> Bool
-- >>> :t specializeAllAsInt (\x y -> x)
-- specializeAllAsInt (\x y -> x) :: Int -> Int -> Int
-- >>> :t specializeAllAsInt fmap
-- specializeAllAsInt fmap
--   :: Functor f => (Int -> Int) -> f Int -> f Int
-- >>> :t specializeAllAsList fmap
-- specializeAllAsList fmap :: (a -> b) -> [a] -> [b]
-- >>> :t specializeAllAsInt "abc"
-- specializeAllAsInt "abc" :: [Char]
-- >>> :t specializeAllAsInt 3
-- specializeAllAsInt 3 :: Int

data family Var (i :: Nat) :: k

class EnumerateWith (i :: Nat) (j :: Nat) (y :: b) | i y -> j
instance {-# INCOHERENT #-}
    ( x ~ Var i
    , is ~ SpecializesAs b b x y
    , IsSpecializable is x y
    , j ~ If is (i + 1) i
    ) => EnumerateWith i j (y :: b)
instance (EnumerateWith i j f, EnumerateWith j k x) => EnumerateWith i k (f x)

infixl 4 :$
data MaterializedType
    = Var Integer
    | MaterializedType :$ MaterializedType
    | Arrow
    | Meta String

class MaterializeType (a :: k) where
    materializeType :: proxy a -> MaterializedType

instance {-# OVERLAPPING #-} (KnownNat i) => MaterializeType (Var i) where
    materializeType _ = Var (natVal @i Proxy)

instance MaterializeType (->) where
    materializeType _ = Arrow

instance {-# OVERLAPS #-} (MaterializeType f, MaterializeType a) => MaterializeType (f a) where
    materializeType _ = materializeType (Proxy @f) :$ materializeType (Proxy @a)

instance {-# OVERLAPPABLE #-} Typeable any => MaterializeType any where
    materializeType = Meta . show . typeRep

instance Show MaterializedType where
    showsPrec p e = case e of
       Var i           -> showParen (p > 10) . showString $ "x_" ++ show i where
       Arrow :$ x :$ y -> showParen (p > 2) $ showsPrec 3 x . showString " -> " . showsPrec 2 y
       Arrow           -> showParen (p > 10) $ showString "(->)"
       f :$ x          -> showParen (p > 9) $ showsPrec 9 f . showString " " . showsPrec 10 x
       Meta name       -> showParen (p > 10) $ showString name

materializeTypeOf :: forall a k. (MaterializeType a, EnumerateWith 0 k a) => a -> MaterializedType
materializeTypeOf _ = materializeType $ Proxy @a

instance Eq (Var i)
instance Num (Var i)
instance Foldable (Var i)
instance Bifunctor (Var i)

-- >>> materializeTypeOf $ \x y -> x
-- x_0 -> x_1 -> x_0
-- >>> materializeTypeOf $ let fix f = f (fix f) in fix
-- (x_0 -> x_0) -> x_0
-- >>> materializeTypeOf bimap
-- (x_0 -> x_1) -> (x_2 -> x_3) -> x_4 x_0 x_2 -> x_4 x_1 x_3
-- >>> materializeTypeOf elem
-- x_0 -> x_1 x_0 -> Bool
-- >>> materializeTypeOf map
-- (x_0 -> x_1) -> [] x_0 -> [] x_1
-- >>> materializeTypeOf 3
-- x_0

class (x :: a) `Elem` (xs :: [a])
type family x `ElemMatch` xs :: Constraint where
    x `ElemMatch` (x ': xs) = ()
    x `ElemMatch` (_ ': xs) = x `Elem` xs
instance (xs ~ (x' ': xs'), TrySpecializeAs x x', x `ElemMatch` xs) => x `Elem` xs

specializeAsEmptyList :: SpecializeAllAs ('[] :: [Symbol]) a => a -> a
specializeAsEmptyList = id

xsHasA :: "a" `Elem` xs => Proxy xs
xsHasA = Proxy

xsHasB :: "b" `Elem` xs => Proxy xs
xsHasB = Proxy

-- >>> :t xsHasA
-- xsHasA :: Proxy ("a" : xs')
-- >>> :t xsHasB
-- xsHasB :: Proxy ("b" : xs')
-- >>> :t [xsHasA, xsHasB]
-- [xsHasA, xsHasB] :: [Proxy ("a" : "b" : xs')]
-- >>> :t let xs = [xsHasB, xsHasA] in specializeAsEmptyList xs
-- let xs = [xsHasB, xsHasA] in specializeAsEmptyList xs
--   :: [Proxy '["b", "a"]]