Trying to map from a type level list to a value level list. Does not type check so far.

Derp.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}

module Derp where

import Data.Kind (Type, Constraint)
import Data.Proxy ( Proxy(Proxy) )
import GHC.TypeLits (Nat, ErrorMessage (ShowType))

type family AllFoo (xs :: [Type]) :: Constraint where
  AllFoo '[] = ()
  AllFoo (x ': xs)  = (Foo x, AllFoo xs)

data Pipeline1
data Pipeline2
type Ps = '[Pipeline1, Pipeline2]

class Foo a where
  foo :: Proxy a -> Int

fooWrap :: forall a. Foo a => Int
fooWrap = foo (Proxy @a)

instance Foo Pipeline1 where
  foo _ = 1

instance Foo Pipeline2 where
  foo _ = 2

-- pulled the Foo constraint into this for now while trying to make it work at all
typeListMap ::
  forall (list :: [Type]) result.
  (
    KnownList list,
    AllFoo list
  ) =>
  (forall (a :: Type). Foo a => result) ->
  [result]
typeListMap f = unconsKnownList @Type @list [] go where
  go ::
    forall l (x :: Type) r.
    (l ~ (x ': r), KnownList r, AllFoo r, Foo x) =>
    Proxy x ->
    Proxy r ->
    [result]
  go (Proxy :: Proxy t) (Proxy :: Proxy ts) = f @t : unconsKnownList @Type @ts [] go

-- copied from polysemy
class KnownList (l :: [k]) where
  unconsKnownList ::
    (l ~ '[] => a) ->
    ( forall x r.
      (l ~ (x ': r), KnownList r) =>
      Proxy x ->
      Proxy r ->
      a
    ) ->
    a

-- copied from polysemy
instance KnownList '[] where
  unconsKnownList b _ = b
  {-# INLINE unconsKnownList #-}

-- copied from polysemy
instance KnownList r => KnownList (x ': r) where
  unconsKnownList _ b = b Proxy Proxy
  {-# INLINE unconsKnownList #-}

{- fails to typecheck here
Derp.hs:81:24: error:
    • Could not deduce (Foo a0) arising from a use of ‘fooWrap’
      from the context: Foo a
        bound by a type expected by the context:
                   forall a. Foo a => Int
        at Derp.hs:81:24-30
      The type variable ‘a0’ is ambiguous
      These potential instances exist:
        two instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the second argument of ‘typeListMap’, namely ‘fooWrap’
      In the expression: typeListMap @Ps fooWrap
      In an equation for ‘derp’: derp = typeListMap @Ps fooWrap
-}
derp = typeListMap @Ps fooWrap