Type-level recursion and PolyKinds

Question

I'm trying to implement a polymorphic function that essentially traverses a type, accumulating a Tag value. I'd like users to be able to do e.g. rec ((1,2), ('a', 3)).

{-# LANGUAGE KindSignatures, PolyKinds, FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Proxy

newtype Tag (a :: k) = Tag Int
    deriving (Eq, Read, Show)

-- My users only have to define their own instances of this class...
class Tagged (a :: k) where
  tag :: Tag a

-- ...like these:
instance Tagged Int where
  tag = Tag 1

instance Tagged Char where
  tag = Tag 2

instance Tagged (,) where
  tag = Tag 3


-- While this is a morally "closed" class; implementing recursion over
-- components of types. This is what I'm struggling with:
class Rec (a :: k) where
  rec :: proxy a -> Tag a

instance (Rec ab, Rec c)=> Rec (ab c) where
  rec _ = let Tag ab = rec Proxy :: Tag ab
              Tag c = rec Proxy :: Tag c
           in Tag (ab * c)

instance {-# OVERLAPPABLE #-} Tagged a=> Rec a where
  rec _ = tag :: Tag a

I've fiddled with this in various ways, and in the current incarnation get the error (for both ab and c, in the first instance):

    • Could not deduce (Tagged ab) arising from a use of ‘rec’
      from the context: (Rec ab, Rec c)
        bound by the instance declaration at flook.hs:26:10-37
    • In the expression: rec Proxy :: Tag ab
      In a pattern binding: Tag ab = rec Proxy :: Tag ab
      In the expression:
        let
          Tag ab = rec Proxy :: Tag ab
          Tag c = rec Proxy :: Tag c
        in Tag (ab * c)
   |
27 |   rec _ = let Tag ab = rec Proxy :: Tag ab
   |                        ^^^^^^^^^

I'm a little surprised at this error since it seems to indicate the second base case instance was selected a priori in the body of the first instance.

Is there a way to get this to work, or a better approach?

Why do you use a proxy for one class and not the other? – Daniel Wagner Oct 10 '18 at 18:05 — Daniel Wagner, Oct 10 '18 at 18:05

score 2 · Accepted Answer · answered Oct 10 '18 at 18:19

I think you should skip having two classes. Just one suffices.

The drawback is that your users won't be able to write instances corresponding to instance Tagged (Maybe Int) in your design which do something special for compound types... but they already couldn't really use those, since the application instance for Rec would always overlap it anyway.

So, without further ado:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Tagged

class Rec a where rec :: Tagged a Int

-- it is still possible for users to define their own instances for base types
instance Rec Int  where rec = 1
instance Rec Char where rec = 2
instance Rec (,)  where rec = 3

instance (Rec ab, Rec c) => Rec (ab c) where
  rec = retag (rec :: Tagged ab Int) * retag (rec :: Tagged c Int)

In ghci:

> rec :: Tagged ((Int, Int), Char) Int
Tagged 18

Oh, yeah this is much better, thanks. It hadn't occurred to me that I wouldn't actually need overlapping instances with this approach as well — jberryman, Oct 10 '18 at 19:55

Type-level recursion and PolyKinds

1 Answers1