Nested Type-Level Programming

Question

I'm attempting to use DataKinds to do type-level programming, but am running into difficulties when I have one of these structures nested in another.

{-# LANGUAGE DataKinds, TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances #-}

module Temp where

data Prop1 = D | E 

data Lower :: Prop1 -> * where
  SubThing1 :: Lower D
  SubThing2 :: Lower E

class ClassLower a where
  somefunc2 :: a -> String

instance ClassLower (Lower D) where
  somefunc2 a = "string3"

instance ClassLower (Lower E) where
  somefunc2 a = "string4"

data Prop2 = A | B | C

data Upper :: Prop2 -> * where
  Thing1 :: Upper A
  Thing2 :: Upper B
  Thing3 :: Lower a -> Upper C

class ClassUpper a where
  somefunc :: a -> String

instance ClassUpper (Upper A) where
  somefunc a = "string1"

instance ClassUpper (Upper B) where
  somefunc a = "string2"

instance ClassUpper (Upper C) where
  somefunc (Thing3 x) = somefunc2 x

As soon as I add that last instance of ClassUpper, I end up with an error.

Temp.hs:37:25: error:
    • Could not deduce (ClassLower (Lower a))
        arising from a use of ‘somefunc2’
      from the context: 'C ~ 'C
        bound by a pattern with constructor:
                   Thing3 :: forall (a :: Prop1). Lower a -> Upper 'C,
                 in an equation for ‘somefunc’
        at /Users/jdouglas/jeff/emulator/src/Temp.hs:37:13-20
    • In the expression: somefunc2 x
      In an equation for ‘somefunc’: somefunc (Thing3 x) = somefunc2 x
      In the instance declaration for ‘ClassUpper (Upper 'C)’

I understand that 'C ~ 'C indicates type equality, but I don't understand what the underlying problem is, much less the solution or workaround.

What am I not understanding, and what is the best way to tackle this problem?

Answer 1

Or you could write out your ClassLower instance like this, using pattern matching (rather than the type variable) to distinguish the cases of the GADT:

instance ClassLower (Lower a) where
    somefunc2 SubThing1 = "string3"
    somefunc2 SubThing2 = "string4"

Answer 2

The problem here is a bit subtle. The reason one might expect GHC to accept this is that you have instances for all possible Lower a since you only provide ways of making Lower D and Lower E. However, one could construct a pathological definition for Lower like

import GHC.Exts (Any)

data Lower :: Prop1 -> * where
  SubThing1 :: Lower D
  SubThing2 :: Lower E
  SubThing3 :: Lower Any

The point is that not only D and E have kind Prop1. It isn't just with things like Any that we can play such shenanigans - even the following constructor is allowed (so F Int :: Prop1 too)!

  SubThing4 :: Lower (F Int)

type family F x :: Prop1 where {}

So, in summary, the underlying problem is that GHC really can't be sure that the ClassLower (Lower a) constraint (needed due to the use of somefunc2) is going to be satisfied. To do so, it would have to do a fair bit of work checking the GADT constructors and making sure that every possible case is covered by some instance.

In this case, you could solve your problem by adding the ClassLower (Lower a) constraint to the GADT constructor (an enabling FlexibleContexts).

data Upper :: Prop2 -> * where
  Thing1 :: Upper A
  Thing2 :: Upper B
  Thing3 :: ClassLower (Lower a) => Lower a -> Upper C