How can I make a typeclass to represent containers containing extractable `Num` instance types?

Question

I've been struggling with expressing a certain pattern in Haskell's type system for some time now. I am even having a hard time explaining it (I guess I don't understand the problem well enough to formulate it), but here goes! (And thanks in advance to any intrepid adventurers who can make sense of and answer my question!)

Let's pretend that we have two different container types, ContF and ContD, each of which is just an ADT holding a single value of Float and Double, respectively (they may as well be newtypes in this example).

We want to write a polymorphic function that works on either type. Maybe it extracts the value and adds 1 to it (so we have a Num constraint). So we create a typeclass, Cont, with a function for extracting the value.

We cannot just have the num prototype as num :: (Num n) => t -> n, because then we would get "cannot deduce Float ~ n" compile-time errors; so we introduce an associated type family.

{-# LANGUAGE TypeFamilies #-}

data ContF = CF Float
data ContD = CD Double

class Cont t where
    type family ContNum t :: *
    num :: t -> ContNum t

instance Cont ContF where
    type ContNum ContF = Float
    num (CF f) = f

instance Cont ContD where
    type ContNum ContD = Double
    num (CD d) = d

contAdd1 :: (Cont t, Num n) => t -> n
contAdd1 t = num t + 1

However, when I try to compile this I get the following error.

Could not deduce (n ~ ContNum t)
from the context (Cont t, Num n)
  bound by the type signature for contAdd1 :: (Cont t, Num n) => t -> n

Maybe what I am trying to ask is: How do I make a typeclass to represent containers containing extractable Num instance types? Also, note that this is a very contrived example to demonstrate what I hope to understand.

Answer 1

The answer is in the error message. You need to tell somehow to the compiler that n is in fact ContNum.

You can do

contAdd1:: (Cont t, Num n, n ~ ContNum t) => t -> n

or don't use n at all

contAdd1 :: (Cont t, Num (ContNum t)) => t -> ContNum t

But the last one needs the FlexibleContexts extension.

This was the first part of your question, how to make it compile. To answer your question about how to move the constraint at a type class level ? Just add it. It works :-)

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}

data ContF = CF Float
data ContD = CD Double

class Num (ContNum t) =>  Cont t where
    type family ContNum t :: *
    num :: t -> ContNum t

instance Cont ContF where
    type ContNum ContF = Float
    num (CF f) = f

instance Cont ContD where
    type ContNum ContD = Double
    num (CD d) = d

contAdd1 :: (Cont t) => t -> ContNum t
contAdd1 t = num t + 1



> contAdd1 (CF 4)
 5.0