In Haskell how can I match a type class with an instance of that type class?

Question

I have defined the following classes:

class Configuration c where
  input :: (PortIn pin, Show pin) => c -> pin
  startSt :: (SysState st, Show st) => c -> st

class (Eq pin, Show pin) => PortIn pin

class (Eq st, Show st) => SysState st

The following types and instances:

--inputs
data PIn = PIn { _clk   :: Bit
               , _reset :: Bool
               , _start :: Bool
               , _stop  :: Bool
               } deriving (Eq)
instance PortIn PIn
instance Show PIn where
  show PIn {..} =
    "PIn\n\t _clk = " P.++ show _clk
    P.++ "\n\t _reset = " P.++ show _reset
    P.++ "\n\t _start = " P.++ show _start
    P.++ "\n\t _stop = " P.++ show _stop

--Outputs and state data
data St = St { _cnt_en   :: Bool
             , _count_us :: BitVector 4
             , _stop_d1  :: Bool
             , _stop_d2  :: Bool
             , _count    :: BitVector 4
             } deriving (Eq)

instance SysState St
instance Show St where
 show St {..} =
        "St\n\t _cnt_en = " P.++ show _cnt_en

   P.++ "\n\t _count_us = " P.++ show _count_us
   P.++ "\n\t _stop_d1 = " P.++ show _stop_d1
   P.++ "\n\t _stop_d2 = " P.++ show _stop_d2
   P.++ "\n\t _count = " P.++ show _count

Why am I unable to create an instance of Configuration here:

data Config = Config { input'  :: PIn
                     , startSt' :: St
                     } deriving (Eq)

instance Show Config where
 show Config {..} =
        "Config:\n input = " P.++ show input'
   P.++ "\n startSt = " P.++ show startSt'

instance Configuration Config where
  input = input'
  startSt = startSt'

I get the following error:

Couldn't match type ‘pin’ with ‘PIn’
  ‘pin’ is a rigid type variable bound by
        the type signature for
          input :: (PortIn pin, Show pin) => Config -> pin
        at Clks_n_regs_4.hs:101:3
Expected type: Config -> pin
  Actual type: Config -> PIn
Relevant bindings include
  input :: Config -> pin (bound at Clks_n_regs_4.hs:101:3)
In the expression: input'
In an equation for ‘input’: input = input'

I would think I can use input' because it results in a PIn which in an instance of pin.

I have a misunderstanding somewhere, hopefully someone can explain what I am missing.

Answer 1

To understand why your code does not type check perhaps see: existential vs. universally quantified types. To make this work, one possibility would be to use Functional Dependencies. Then your type-class would be:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}

class (PortIn pin, Show pin, SysState st, Show st) => Configuration c pin st
    | c -> pin, c -> st where
  input   :: c -> pin
  startSt :: c -> st

and the instance definition would be:

instance Configuration Config PIn St where
  input   = input'
  startSt = startSt'

This will make your code type check, though may not be what you are after.

A different direction would be to use existential types. In that case:

{-# LANGUAGE ExistentialQuantification #-}

data PortInShow   = forall a . (PortIn a,   Show a) => PortInShow a
data SysStateShow = forall a . (SysState a, Show a) => SysStateShow a

class Configuration c where
  input   :: c -> PortInShow
  startSt :: c -> SysStateShow

instance Configuration Config where
  input   = PortInShow   . input'
  startSt = SysStateShow . startSt'

Answer 2

The applicability of the linked question in behzad.nouri's answer might not be clear to someone who doesn't already understand what's going on here. To answer the actual question in more detail:

class Configuration c where
  input :: (PortIn pin, Show pin) => c -> pin
  startSt :: (SysState st, Show st) => c -> st

means that the type of input will be

input :: (Configuration c, PortIn pin, Show pin) => c -> pin

which in turn means the caller of input can choose any types they like for c and pin in the type of input, as long as c is an instance of Configuration and pin is an instance of PortIn and Show. (This is the way all polymorphic functions work: even :: Integral a => a -> Bool means that the caller can apply even to a value of any type that is an instance of Integral, and fromInteger :: Num a => Integer -> a means that the caller can treat the result of fromInteger as having any type that is an instance of Num.)

It follows that you, the implementor of the input method for the Configuration Config, must provide an implementation that works for any type pin that is an instance of PortIn and Show. But your implementation input = input' can only possibly work for the single type PIn. That's why the compiler rejects it. (It tells you that the type pin of the result is a "rigit type variable", meaning you don't get to choose it as the implementor but must assume it has already "rigidly" been chosen by the caller.)

As for what to do about this, you already got a good answer in a comment on the codereview question from Gurkenglas: you can simply parameterize Config and other types as necessary on the type of the ports and states.