Associated type not being resolved, don't know why

Question

This is a simplified example that shows an error I'm getting that I don't understand. It's still a little long, sorry.

--
--  Test of XMaybe and XMonad
--

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Main (main) where

-------------------------------------------------------------------------------

class XMonad (tc :: k -> * -> *) (af :: k) (bf :: k) where
  type XResultT tc af bf :: k
  (>>~)   :: tc af a -> (a -> tc bf b) -> tc (XResultT tc af bf) b

-------------------------------------------------------------------------------

data XMaybe :: Bool -> * -> * where
  XNothing ::      XMaybe False a
  XJust    :: a -> XMaybe True  a

instance XMonad XMaybe False False where
  type XResultT XMaybe False False = False
  (>>~) _ _ = XNothing

instance XMonad XMaybe True False where
  type XResultT XMaybe True False = False
  (>>~) _ _ = XNothing

instance XMonad XMaybe False True where
  type XResultT XMaybe False True = False
  (>>~) _ _ = XNothing

instance XMonad XMaybe True True where
  type XResultT XMaybe True True = True
  (>>~) (XJust x) f = f x

-------------------------------------------------------------------------------

fromXMaybe :: XMaybe t a -> Maybe a
fromXMaybe (XJust x) = Just x
fromXMaybe XNothing  = Nothing

-------------------------------------------------------------------------------

class TestClass a where
  type Enabled a :: Bool
  queryVal :: a -> XMaybe (Enabled a) Int
  queryGet :: a -> XMaybe (Enabled a) (a -> Int)

-------------------------------------------------------------------------------

newtype Test = Test Int  deriving Show

instance TestClass Test where
  type Enabled Test = True
  queryVal (Test x) = XJust x
  queryGet _        = XJust (\(Test x) -> x)

-------------------------------------------------------------------------------

test :: (TestClass a, Show a) => a -> IO ()
test x0 = do
  putStrLn "--------------------"
  putStr   "  x0 = "
  print    x0

  --  This is OK
  let x1 = queryVal x0
  putStr   "  x1 = "
  print $ fromXMaybe x1

  --  This is OK
  let x2 = queryGet x0

  --  This gives a compiler error - (Enabled a) isn't evaluated, so the
  --  instance of XMonad is undetermined, so >>~ is rejected. But AFAICT that
  --  (Enabled a) *should* be evaluated - which TestClass instance doesn't seem
  --  ambiguous...
  --
  --  1.  The instance specifies "type Enabled Test = True"
  --  2.  If it was ambiguous, how come the earlier queryGet call works fine?
  --      Comment out the following two lines and this compiles and runs. Isn't
  --      an ambiguous result type automatically a compile-time error?
  --
  let x3 = queryGet x0 >>~ \get ->
           XJust $ get x0

  putStrLn "--------------------"

-------------------------------------------------------------------------------

main :: IO ()
main = test (Test 3)

-------------------------------------------------------------------------------

Here's the specific error from GHC 7.10.3...

[1 of 1] Compiling Main             ( test03.hs, test03.o )

test03.hs:91:24:
    Could not deduce (XMonad XMaybe (Enabled a) 'True)
      arising from a use of ‘>>~’
    from the context (TestClass a, Show a)
      bound by the type signature for
                 test :: (TestClass a, Show a) => a -> IO ()
      at test03.hs:67:9-43
    In the expression: queryGet x0 >>~ \ get -> XJust $ get x0
    In an equation for ‘x3’:
        x3 = queryGet x0 >>~ \ get -> XJust $ get x0
    In the expression:
      do { putStrLn "--------------------";
           putStr "  x0 = ";
           print x0;
           let x1 = queryVal x0;
           .... }

Basically, a class instance hasn't been deduced because an associated type hasn't been evaluated. But the >>~ operator that triggers the problem just picks up that type information from its first argument. The same associated type seems to be evaluated just fine for the exact same type, determining the result type from queryVal and queryGet, just so long as that result isn't passed as the first argument to >>~.

From some messing around I did using the type-level naturals features a little while ago, I get the feeling there's a constraint missing from my test function - something like KnownBool (Enabled a) - but so far as I can tell no such thing exists.

So - what am I doing wrong?

Explanation of where this comes from - XMaybe is meant to be like Maybe, but with statically-resolved type-level knowledge of whether XJust or XNothing applies. It can be a Monad instance with all laws respected, which should abstract away all the clutter, but it doesn't work like Maybe that way - the sequenced actions would have to be either all XJust or all XNothing, so having a mixture would be a type error as opposed to an XNothing result. So XMonad is a monad-ish class that allows an extra type argument to vary, and >>~ is a bind-ish operator. There's no equivalent of return due to ambiguity issues - for now I'm just using the XJust constructor instead.

As there's only one instance, the XMonad class might be redundant and is certainly more general that it needs to be for this (though the lack of a return breaks that generality), but I want to see where the type-varying-monadish-things journey ends - possibly with IxMonad, possibly with something similar but slightly different, though at the moment I don't know much more about IxMonad than that it exists.

In the meantime, I'm stuck on this compiler error.

---

Based on the answer and comments from @dfeuer below, but not using the KnownBool solution as I figure XMaybe should know the Bool anyway...

--
--  Test of XMaybe and XMonad
--

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

module Main (main) where

-------------------------------------------------------------------------------

type family BoolAnd a b :: Bool where
  BoolAnd True  a = a
  BoolAnd False a = False

-------------------------------------------------------------------------------

class XMonad (tc :: k -> * -> *) (af :: k) (bf :: k) where
  type XResultT tc af bf :: k
  (>>~)   :: tc af a -> (a -> tc bf b) -> tc (XResultT tc af bf) b

-------------------------------------------------------------------------------

data XMaybe :: Bool -> * -> * where
  XNothing ::      XMaybe False a
  XJust    :: a -> XMaybe True  a

--  Polymorphism problem in `test` resolved by only having one instance of
--  `XMonad` for `XMaybe`. Still need ResultT to tell the class which type to
--  use for (>>~), but can compute that for all cases with a more generally
--  useful indexed type family. The implementation cases for (>>~) are handled
--  by normal pattern-matching.
--
--  Question - can the compiler optimise away run-time costs for this seemingly
--             resolvable-at-compile-time data constructor matching?
--
--    I suspect not, if only because of the possibility that the first argument
--    is undefined, so that data constructor cannot be forced. It's slightly
--    unfortunate if I'm right - although it's not the main point, one reason
--    for knowing whether XJust or XNothing applies at the type level is to
--    avoid those overheads. Conceptually, `XMaybe` is a compile-time choice
--    between two newtypes. XNothing has no components, but you could add a ()
--    component. The GADT implementation here presumably means the newtype cost
--    model doesn't apply.
instance XMonad XMaybe af bf where
  type XResultT XMaybe af bf = BoolAnd af bf
  (>>~) XNothing  _ = XNothing
  (>>~) (XJust x) f = f x

instance Show a => Show (XMaybe f a) where
  show (XJust x) = "XJust (" ++ (show x) ++ ")"
  show XNothing  = "XNothing"

-------------------------------------------------------------------------------
--  Deliberately not using Proxy here.
--
--  The idea is that get and put are optional interfaces. You query for those
--  interfaces in a vaguely COM-like sense, with usage patterns similar to the
--  three examples in the `test` function below, and you do that just before
--  using those interfaces.
--
--  The only reason `get` and `put` aren't provided directly as class members
--  is they might not exist (with the assumption that having lots of classes
--  and lots of constraints would be impractical). So you `queryGet` and/or
--  `queryPut` to access the relevant functions if they exist.
--
--  Since the value you call `queryGet` for is the same value you call `get`
--  for, you should always have a suitable value of the correct type to pass to
--  `queryGet`. So you should be able to write `queryGet x`, as opposed to
--  `queryGet (Proxy :: Proxy a).
--
--  In short, even though `queryGet` and co. don't use the value of their first
--  argument, life is IMO easier in this case if you pretend they do.
--
--  Also, maybe for some other instance, they will - which function *could* be
--  chosen based on the run-time value and that's perfectly valid, even if that
--  option is rarely or never used.

class TestClass a where
  type GetEnabled a :: Bool
  type PutEnabled a :: Bool
  queryGet :: a -> XMaybe (GetEnabled a) (a -> Int)
  queryPut :: a -> XMaybe (PutEnabled a) (a -> Int -> a)

-------------------------------------------------------------------------------

newtype TestA = TestA Int  deriving Show
newtype TestB = TestB Int  deriving Show
newtype TestC = TestC Int  deriving Show

instance TestClass TestA where
  type GetEnabled TestA = True
  type PutEnabled TestA = True
  queryGet _ = XJust (\(TestA x) -> x)
  queryPut _ = XJust (\(TestA x) y -> TestA (x + y))

instance TestClass TestB where
  type GetEnabled TestB = False
  type PutEnabled TestB = True
  queryGet _ = XNothing
  queryPut _ = XJust (\(TestB x) y -> TestB (x + y))

instance TestClass TestC where
  type GetEnabled TestC = True
  type PutEnabled TestC = False
  queryGet _ = XJust (\(TestC x) -> x)
  queryPut _ = XNothing

-------------------------------------------------------------------------------

test :: ( TestClass a, Show a
        ) => a -> IO ()
test x0 = do
  putStrLn "--------------------"
  putStr   "  x0 = "
  print    x0

  let x1 = queryGet x0 >>~ \get ->
           XJust $ get x0
  putStr   "  x1 (using get only) = "
  print x1

  let x2 = queryPut x0 >>~ \put ->
           XJust $ put x0 13
  putStr   "  x2 (using put only) = "
  print x2

  let x3 = queryGet x0 >>~ \get ->
           queryPut x0 >>~ \put ->
           XJust $ (get x0, put x0 13)
  putStr   "  x3 (using get and put) = "
  print x3

  putStrLn "--------------------"

-------------------------------------------------------------------------------

main :: IO ()
main = do test (TestA 3)
          test (TestB 4)
          test (TestC 5)

-------------------------------------------------------------------------------

Answer 1

The problem is as GHC indicates. test is polymorphic in a, so within test there's no way to determine what Enabled a actually is, and therefore no way to choose an XMonad instance. You also don't have an XMonad constraint abstracting that away, so it doesn't compile. You could easily use the sort of "known Bool" you mention:

data SBool (b :: Bool) where
  SFalse :: SBool 'False
  STrue :: SBool 'True

class KnownBool (b :: Bool) where
  knownBool :: SBool b

instance KnownBool 'False where
  knownBool = SFalse

instance KnownBool 'True where
  knownBool = STrue

Adding such a context would let you pattern match on knownBool to reveal the Bool type argument and therefore the appropriate XMonad instance. You could even write just one XMonad instance for all the maybeish things using two KnownBool constraints.

---

Side notes

If you're never going to use a certain argument, make it a proxy:

class TestClass a where
  type Enabled a :: Bool
  queryVal :: a -> XMaybe (Enabled a) Int
  queryGet :: proxy a -> XMaybe (Enabled a) (a -> Int)

This makes it much easier to call the queryGet function.

Even if you want multiple instances of XMonad (the main reason I can think of is to get certain inlining behavior), you can still reduce their number:

instance XMonad XMaybe 'False b where
  type XResultT XMaybe 'False b = 'False
  (>>~) _ _ = XNothing

instance XMonad XMaybe 'True 'False where
  type XResultT XMaybe 'True 'False = 'False
  (>>~) _ _ = XNothing

instance XMonad XMaybe 'True 'True where
  type XResultT XMaybe 'True 'True = 'True
  (>>~) (XJust x) f = f x