haskell constraint families

haskell, types

Solution

There's a few odd things going on in your definition. First of all, the class variable `f` is never mentioned in the type of the (only) class method `next`. How is the compiler supposed to choose which instance of the type class to use? I'm going to assume you meant this:

{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
module Test where

import GHC.Exts  -- to get Constraint type constructor

class NextClass f where
    type Ctxt f :: Constraint
    next :: Ctxt f => f -> f

instance NextClass Int where
    type Ctxt Int = Num Int
    next b = b + 1

n :: (NextClass a) => a -> a
n v = next v

The next oddity is that `Int` already has a `Num` instance, so this isn't much of a constraint. But let's leave that aside for now (since it doesn't affect the error we get) and just look at the new error:

test.hs:15:7:
    Could not deduce (Ctxt a) arising from a use of `next'
    from the context (NextClass a)
      bound by the type signature for n :: NextClass a => a -> a
      at test.hs:15:1-12
    In the expression: next v
    In an equation for `n': n v = next v

Actually, this error looks quite sensible: the whole point of the constraint is that having an instance for `NextClass a` isn't enough; we must also have an instance of `Ctxt a`. So we can fix up the type signature:

n :: (NextClass a, Ctxt a) => a -> a
n v = next v

...and then it compiles. The final oddity is that this is a particularly degenerate use of constraint kinds, since this simpler code is essentially equivalent:

class NextClass f where
    next :: f -> f

instance Num Int => NextClass Int where
    next b = b + 1

...and the translation from the previous thing to the new thing is quite mechanical: instead of declaring `instance NextClass {- foo -} where type Ctxt {- foo -} = {- bar -}`, you just write `instance {- bar -} => NextClass {- foo -}` instead.

Problem

Original source