PolyVar.hs

#! /usr/bin/env nix-shell
#! nix-shell -i ghci -p "pkgs.haskellPackages.ghcWithPackages(p: [p.constraints])"
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}

import Data.Kind
import Data.Type.Equality (type (==), (:~:)(Refl))
import Data.Type.Bool (If)
import Data.Proxy (Proxy (..))
import Unsafe.Coerce (unsafeCoerce)
import Data.Typeable (Typeable, TypeRep, typeOf, eqT)
import Data.Constraint (Dict (..), withDict)
data Sum :: [*] -> * where
  Sum :: forall a as. (Typeable a, Member a as) => a -> Sum as

hif :: forall a b (xs :: [*]). (Typeable a, Typeable b, Member a xs, Member b xs) => Bool -> a -> b -> Sum xs
hif True a _ = Sum a
hif False _ b = Sum b


data Handler (as :: [*]) (r :: *) :: * where
  End :: forall r. Handler '[] r
  Handle :: forall a r as. Typeable a => (a -> r) -> Handler as r -> Handler (a : as) r

type family Concat (as :: [k]) (bs :: [k]) :: [k] where
  Concat '[] bs = bs
  Concat (a ': as) bs = a ': Concat as bs

type family IsMember (a :: k) (as :: [k]) where
  IsMember a '[] = False
  IsMember a (a : as) = True
  IsMember a (b : as) = IsMember a as

type Member a as = IsMember a as ~ True

type ConcatAssoc as bs cs = Concat as (Concat bs cs) ~ Concat (Concat as bs) cs
concatAssoc :: forall as bs cs. Dict (ConcatAssoc as bs cs)
concatAssoc = unsafeCoerce (Dict :: Dict (Int ~ Int))

match :: forall as bs r. Sum (Concat as bs) -> Proxy as -> Handler bs r -> r
match s ls rs =
  case rs of
    End -> error "impossible"
    Handle (f :: a -> r) (next :: Handler xs r) -> case s of
      Sum (a :: b) -> case eqT :: Maybe (a :~: b) of
        Nothing -> withDict (concatAssoc @as @'[a] @xs) $
          match s (Proxy :: Proxy (Concat as '[a])) next
        Just Refl -> f a

Could not deduce: Concat (Concat as '[a]) as1 ~ Concat as (a : as1)

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

import Data.Kind
import Data.Type.Equality ((:~:)(Refl))
import Data.Proxy (Proxy (..))
import Data.Typeable (Typeable, eqT)
import Data.Constraint

main = return ()

type family Concat (as :: [k]) (bs :: [k]) :: [k] where
  Concat '[] bs = bs
  Concat (a ': as) bs = a ': Concat as bs

type family IsMember (a :: k) (as :: [k]) where
  IsMember a '[] = False
  IsMember a (a : as) = True
  IsMember a (b : as) = IsMember a as

type Member a as = IsMember a as ~ True

data Sum :: [*] -> * where
  Sum :: forall a as. (Typeable a, Member a as) => a -> Sum as

class ConcatAssoc (as :: [k]) (bs :: [k]) (cs :: [k]) where
  concatAssoc :: Proxy as -> Proxy bs -> Proxy cs -> Dict (Concat as (Concat bs cs) ~ Concat (Concat as bs) cs)

instance ConcatAssoc '[] bs cs where
  concatAssoc _ _ _ = Dict

instance forall a as bs cs. ConcatAssoc as bs cs => ConcatAssoc (a : as) bs cs where
  concatAssoc _ _ _ = case concatAssoc (Proxy :: Proxy as) (Proxy :: Proxy bs) (Proxy :: Proxy cs) of
    Dict -> Dict

class ConcatAssoc (as :: [k]) (bs :: [k]) (cs :: [k]) where
  concatAssoc :: Dict (Concat as (Concat bs cs) ~ Concat (Concat as bs) cs)

instance ConcatAssoc '[] bs cs where
  concatAssoc = Dict

instance forall a as bs cs. ConcatAssoc as bs cs => ConcatAssoc (a : as) bs cs where
  concatAssoc = case concatAssoc @_ @as @bs @cs of Dict -> Dict