Haskell hobbyist here - is it possible to map a polymorphic constant over a list of types in a generic way?

More precisely, consider this snippet:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
  
module Main where

import Data.Kind( Type )

class HasName a where name :: String

instance HasName Int where name = "Int"

instance HasName Double where name = "Double"


class AllNames (ts :: [Type]) where
  allNames :: [String]

instance AllNames '[] where
  allNames = []

instance (HasName t, AllNames rest) => AllNames (t ': rest) where
  allNames = name @t : allNames @rest

  
main :: IO ()
main = print $ allNames @'[Int, Double]

Unsurprisingly, this works as expected, i.e., it prints ["Int","Double"]. However, if I try to generalize the pattern above so that the code can be used with any name-like polymorphic constant, then I run into problems.

Here's my attempt at generalization:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
  
module Main where

import Data.Kind( Constraint, Type )

--
-- Intended to be the generalized version of 'name'
--
type PolymorphicConstant (c :: Type -> Constraint) (a :: Type) = forall t . c t => a

--
-- Intended to be the generalized version of 'AllNames'
--
class AllPolymorphicConstants (c :: Type -> Constraint) (ts :: [Type]) (a :: Type) where
  allPolymorphicConstants :: PolymorphicConstant c a -> [ a ]

instance AllPolymorphicConstants c '[] a where
  allPolymorphicConstants _ = []

instance (c t, AllPolymorphicConstants c rest a) => AllPolymorphicConstants c (t ': rest) a where
  allPolymorphicConstants f = f @t : allPolymorphicConstants @c @rest @a f

Alas, this doesn't compile (btw, I'm using GHC 8.10.7):

Main.hs:31:74: error:
    • Could not deduce: c t0 arising from a use of ‘f’
      from the context: (c t, AllPolymorphicConstants c rest a)
        bound by the instance declaration at Main.hs:30:10-91
      or from: c t1
        bound by a type expected by the context:
                  PolymorphicConstant c a
        at Main.hs:31:74
    • In the fourth argument of ‘allPolymorphicConstants’, namely ‘f’
      In the second argument of ‘(:)’, namely
        ‘allPolymorphicConstants @c @rest @a f’
      In the expression: f @t : allPolymorphicConstants @c @rest @a f
    • Relevant bindings include
        f :: PolymorphicConstant c a (bound at Main.hs:31:27)
        allPolymorphicConstants :: PolymorphicConstant c a -> [a]
          (bound at Main.hs:31:3)
   |
31 |   allPolymorphicConstants f = f @t : allPolymorphicConstants @c @rest @a f
   |                                                                          ^

I'm probably missing something basic that makes this sort of generalization impossible - but what is it exactly?

CodePudding user response：

I wish someone can prove me wrong, but this is one of the few corner cases where we meet a limitation of current GHC and we can not get away from using Proxy, Tagged or similar "relics" of the past.

A minimal example

Let's consider a simpler example:

class C a where

-- Ambiguous type
type T a = forall t. C t => a

Note that, if we have a value x :: T a, there is no unambiguous way to use it except with an explicit type argument x @t. That's the price to pay for using ambiguous types, but that's fine.

The following code type-checks as expected.

foo :: forall t a. (C t) => T a -> a
foo f = f @t

Instead, this does not.

-- Error: Could not deduce (C t0) arising from a use of `foo'
foo2 :: forall t a. (C t) => T a -> a
foo2 = foo

This might be surprising at first. Indeed, foo2 has exactly the same type of foo, so foo2=foo is obviously OK! Yet, it fails. The reason is, once again, ambiguous types, and the thumb rule still is: if something has an ambiguous type, we can not use it if we don't pass additional @t @a arguments.

Doing that makes everything work.

foo3 :: forall t a. (C t) => T a -> a
foo3 = foo @t @a

The above is a little strange since we can't write (and have not to write) foo3 @t @a = foo @t @a. I guess that if GHC forced us to do that, then it could also allow us to "eta-contract the type arguments" everything and write foo3 = foo.

Now, what if we eta-expand the value argument (not the type!). We get an error:

-- Error: Could not deduce (C t0) arising from a use of `x'
foo4 :: forall t a. (C t) => T a -> a
foo4 x = foo @t @a x

Groan. This is simply foo3 = foo @t @a eta-expanded. What's going wrong here? Well, the issue is the same: now we introduced x :: T a, and that's an ambiguous type, so we can not use x without @... arguments. Even if foo expects a polymorphic value!

Here we find ourselves unable to escape. GHC sees the polymorphic arguments and adds an implicit type argument abstraction over x, adding (\@t0 -> ... in front. But that's a kind of syntax we are not allowed to use, and there is no way to capture the fresh type variable t0. In other words, we would like to write

foo4 :: forall t a. (C t) => T a -> a
foo4 x = foo @t @a (\@t0 -> x @t0)

but we can only write

foo4 :: forall t a. (C t) => T a -> a
foo4 x = foo @t @a (x @something)

and there is no way to mention t0 there. Sigh.

Using proxies

The only "solution" I can see it to use Proxy (or similar relics), and avoid ambiguous types.

-- No longer ambiguous
type T a = forall t. C t => Proxy t -> a

foo :: forall t a. (C t) => T a -> a
foo f = f (Proxy @t)

foo4 :: forall t a. (C t) => T a -> a
foo4 x = foo @t @a x

Now we can use x as-is since it has no longer an ambiguous type.

Using Tagged or wrapping the polymorphic value inside a newtype or data would also work, since it makes the type no longer ambiguous.

The original code, proxy-fied

type PolymorphicConstant (c :: Type -> Constraint) (a :: Type) 
   = forall t . c t => Proxy t -> a

--
-- Intended to be the generalized version of 'AllNames'
--
class AllPolymorphicConstants (c :: Type -> Constraint) (ts :: [Type]) (a :: Type) where
  allPolymorphicConstants :: PolymorphicConstant c a -> [ a ]

instance AllPolymorphicConstants c '[] a where
  allPolymorphicConstants _ = []

instance (c t, AllPolymorphicConstants c rest a) 
    => AllPolymorphicConstants c (t ': rest) a where
  allPolymorphicConstants f = f (Proxy @t) : allPolymorphicConstants @c @rest @a f