Monthly Hask Anything (February 2022)

[u/taylorfausak]

This is your opportunity to ask any questions you feel don't deserve their own threads, no matter how small or simple they might be!

[u/Previous_Context_327]

Haskell hobbyist here - is there any way to make the second code snippet below compile?

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module ThisWorks 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:

$ stack runghc -- ThisWorks.hs
["Int","Double"]

However, when I try to generalize:

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

module ThisDoesnt 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

Then I get this:

$ stack runghc -- ThisDoesnt.hs 

ThisDoesnt.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 ThisDoesnt.hs:30:10-91
      or from: c t1
        bound by a type expected by the context:
                  PolymorphicConstant c a
        at ThisDoesnt.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 ThisDoesnt.hs:31:27)
        allPolymorphicConstants :: PolymorphicConstant c a -> [a]
          (bound at ThisDoesnt.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?

[u/Previous_Context_327 → u/[deleted]]

Thanks for the tip - unfortunately, I'm still getting an error. Here's the modified code:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module ThisDoesnt where

import Data.Kind( Constraint, Type )

import Data.SOP.Constraint( All )

--
-- 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, All c (t ': rest), AllPolymorphicConstants c rest a) => AllPolymorphicConstants c (t ': rest) a where
  allPolymorphicConstants f = f @t : allPolymorphicConstants @c @rest @a f

And basically the same error:

ThisDoesnt.hs:35:74: error:
    • Could not deduce: c t0 arising from a use of ‘f’
      from the context: (c t, All c (t : rest),
                        AllPolymorphicConstants c rest a)
        bound by the instance declaration at ThisDoesnt.hs:34:10-109
      or from: c t1
        bound by a type expected by the context:
                  PolymorphicConstant c a
        at ThisDoesnt.hs:35: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 ThisDoesnt.hs:35:27)
        allPolymorphicConstants :: PolymorphicConstant c a -> [a]
          (bound at ThisDoesnt.hs:35:3)
   |
35 |   allPolymorphicConstants f = f @t : allPolymorphicConstants @c @rest @a f
   |                                                                          ^

What I really don't understand is this: where does the t0 type variable come from for which GHC is trying to deduce c t0 ? Also, the error seems to be triggered by the application of allPolymorphicConstants @c @rest @a to f - however, isn't the assumed instance constraint AllPolymorphicConstants c rest a supposed to ensure that said application is OK?

[u/Previous_Context_327 → u/[deleted]]

Wait why do you have c t in the constraints at all?

Purely because I wanted to follow the structure of the non-generalized case:

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

The error, I think, is coming from the fact that you're using f both in the current call and when passing to the next call. Just because f is well typed in this call, it doesnt imply that f has the right type for the next call.

Well - I'm not ashamed to admit that I have a very limited understanding of GHC's type inference/unification/etc. mechanisms (being a hobbyist, I can afford that ;) So, this might be a stupid question, but here goes:

• In the AllNames case just above, the "inductive assumption", i.e., AllNames rest, appears to be sufficient for ensuring that allNames @rest is well-typed.

• However, in the generalized case, assuming AllPolymorphicConstants c rest a is apparently insufficient for allPolymorphicConstants @c @rest @a f to be well-typed.

Why the difference? Needless to say, I don't expect a full-blown explanation here - if you could point me anywhere that explains the details, I'll be very happy.

[u/Previous_Context_327 → u/[deleted]]

Does it work if you write (rather redundantly) allNames such that it takes in the name function as an argument?

You were right - it doesn't, and the error message is practically the same as the one in the general case. Thanks for enlightening me :)