Could not deduce class instance for a type family-CodePudding

I'm currently learning Haskell's typing system, but I'm having some troubles regarding type families and class instances.

Here is my code:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Test() where
import Data.Kind (Type)

data Color = ColorWhite | ColorBlack

type Board :: Color -> Type
data Board c where
  MkBoard :: (PrintableType c) => Board c

type ExBoard :: Type
data ExBoard where
  MkExBoard :: Board t -> ExBoard

type NextColor :: Color -> Color
type family NextColor c where
  NextColor 'ColorWhite = 'ColorBlack
  NextColor 'ColorBlack = 'ColorWhite

class PrintableType a where
  printT :: String

instance PrintableType 'ColorWhite where
  printT = "White"

instance PrintableType 'ColorBlack where
  printT = "Black"

withBoard :: ExBoard -> (forall c. Board c -> a) -> a
withBoard (MkExBoard b) f = f b

printInfo :: ExBoard -> String
printInfo  eb = withBoard eb $ \b@MkBoard -> printTurn b
printTurn :: forall c. PrintableType c => Board c -> String
printTurn _ = printT @c    " turn!"

compute :: Board c ->  Board (NextColor c)
compute _ = MkBoard

-- >>> printInfo $ MkExBoard $ MkBoard @'ColorWhite
-- >>> printInfo $ MkExBoard $ MkBoard @'ColorBlack
-- "White turn!"
-- "Black turn!"

As it is right now, the compute function gives me the error "No instance for (PrintableType (NextColor c)) arising from a use of ‘MkBoard’", which confuses me, as both outputs for NextColor c are already defined as instances of PrintableType.

If I remove the (PrintableType c) from MkBoard, then the printTurn starts giving me the error No instance for (PrintableType c) arising from a use of ‘printTurn’, and the compute doesn't give errors anymore.

Given this, I can only guess that the compiler isn't resolving the class instances for type families results. Is there any way for me to be able to keep the (PrintableType c) in MkBoard, because of the print function, and also be able to solve the problem with the compute function? Or is there anything else that I'm missing here?

CodePudding user response：

GHC doesn't have a mechanism for deducing a constraint for the whole of a type family (i.e., for the whole image of NextColor). In this particular example it would be just a matter of exhaustion through the few possible cases, but in general this is not possible and could waste a lot of compile time to try.

You can add a class for carrying out the proof manually:

class PrintableType c => BoardColor (c :: Color) where
  nextIsColor :: (BoardColor (NextColor c) => r) -> r

instance BoardColor 'ColorWhite where nextIsColor φ = φ
instance BoardColor 'ColorBlack where nextIsColor φ = φ

compute :: forall c . BoardColor c => Board c -> Board (NextColor c)
compute _ = nextIsColor @c MkBoard

You could save some boilerplate by making it instead

{-# LANGUAGE UndecidableSuperClasses #-}

class (PrintableType c, BoardColor (NextColor c)) => BoardColor c

but I don't think this terminates, and anyway undecidable superclasses are a bit unstable.

CodePudding user response：

I find that -- as a general rule -- if GHC can't deduce an instance, giving it a pat on the head and assuring it that the instance is there usually works.

In this case, the pat on the head is adding the exact constraint GHC says it needs to the type signature for compute:

compute :: (PrintableType (NextColor c)) => Board c ->  Board (NextColor c)
compute _ = MkBoard

Here, this typechecks and you're done. In the general case, GHC might complain about yet more missing instances, and you can just keep adding them until the program either typechecks or you start to suspect that you've made a horrible design error and need to rethink your approach.