Why is an instance not picked?

Question

This is an iteration over Type variables in context not fixed? with associated types.

Im' getting the following error message, but I can't figure out why exactly the HasRecipeCase False instance isn't selected - all the other fields (besides the False) should be generic enough so it can pick that instance.

script.hs:126:6: error:
    • No instance for (HasRecipeCase
                         'False
                         M4
                         '[Recipe IO M1 '[M2, M3], Recipe IO M2 '[], Recipe IO M3 '[M4],
                           Recipe IO M4 '[]])
        arising from a use of ‘cook’
    • In the expression: cook cookbook1 :: IO M4
      In an equation for ‘c1’: c1 = cook cookbook1 :: IO M4
    |
126 | c1 = cook cookbook1 :: IO M4
    |      ^^^^^^^^^^^^^^

Script:

#!/usr/bin/env stack
-- stack --resolver lts-11.4 --install-ghc runghc
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE PolyKinds #-}

import Data.Proxy

class HEq (x :: k) (y :: k) (b :: Bool) | x y -> b
instance {-# OVERLAPPING #-} HEq x x True
instance {-# OVERLAPPABLE  #-} False ~ b => HEq x y b

data family HList (l::[*])

data instance HList '[] = HNil
data instance HList (x ': xs) = x `HCons` HList xs

deriving instance Eq (HList '[])
deriving instance (Eq x, Eq (HList xs)) => Eq (HList (x ': xs))

deriving instance Ord (HList '[])
deriving instance (Ord x, Ord (HList xs)) => Ord (HList (x ': xs))

deriving instance Bounded (HList '[])
deriving instance (Bounded x, Bounded (HList xs)) => Bounded (HList (x ': xs))

class HExtend e l where
  type HExtendR e l
  (.*.) :: e -> l -> HExtendR e l

infixr 2 .*.

instance HExtend e (HList l) where
  type HExtendR e (HList l) = HList (e ': l)
  (.*.) = HCons

main = pure ()


newtype Recipe effect target (deps :: [*]) = Recipe { runRecipe :: HList deps -> effect target }

class DefaultRecipe target where
  def :: Recipe target deps effect

type family Foo

class CanCook target (pot :: [*]) where
  type CDeps pot target :: [*]
  cook :: HList pot -> (PotEffect pot) target

instance (HasRecipe target pot, SubSelect pot (CDeps pot target)) => CanCook target pot where
  type CDeps pot target = RDeps pot target
  cook pot =
    let
      deps :: HList deps
      deps = subselect pot
      r :: Recipe (PotEffect pot) target (CDeps pot target)
      r = recipe pot
    in
      runRecipe r $ deps

type family PotEffect (pot :: [*]) :: * -> *
type instance PotEffect (Recipe effect _ _ ': '[]) = effect
type instance PotEffect (Recipe effect _ _ ': Recipe effect _ _ ': '[]) = effect
type instance PotEffect (Recipe effect _ _ ': Recipe effect _ _ ': Recipe effect _ _ ': '[]) = effect
type instance PotEffect (Recipe effect _ _ ': Recipe effect _ _ ': Recipe effect _ _ ': Recipe effect _ _ ': '[]) = effect
type instance PotEffect (Recipe effect _ _ ': Recipe effect _ _ ': Recipe effect _ _ ': Recipe effect _ _ ': Recipe effect _ _ ': '[]) = effect

class HasRecipe target (pot :: [*]) where
  type RDeps pot target :: [*]
  recipe :: HList pot -> Recipe (PotEffect pot) target (RDeps pot target)

class SubSelect (pot :: [*]) (deps :: [*]) where
  subselect :: HList pot -> HList deps

instance SubSelect p d where
  subselect = undefined

class HasRecipeCase (b :: Bool) (target :: *) (pot :: [*]) where
  type RCDeps b target pot :: [*]
  recipeCase :: Proxy b -> Proxy target -> HList pot -> Recipe (PotEffect pot) target (RCDeps b target pot)

instance (PotEffect ((Recipe effect target deps) ': leftoverPot) ~ effect) => HasRecipeCase True target ((Recipe effect target deps) ': leftoverPot) where
  type RCDeps True target ((Recipe effect target deps) ': leftoverPot) = deps
  recipeCase _ _ (HCons head _) = head

instance (HasRecipe target leftoverPot, PotEffect ((Recipe effect target deps) ': leftoverPot) ~ effect, PotEffect leftoverPot ~ effect) =>
  HasRecipeCase False target ((Recipe effect target deps) ': leftoverPot) where
  type RCDeps False target ((Recipe effect target deps) ': leftoverPot) = RDeps leftoverPot target
  recipeCase _ _ (HCons _ tail) = recipe tail

instance (HEq target t bool, HasRecipeCase bool target pot , pot ~ ((Recipe effect t deps) ': leftoverPot)) =>
  HasRecipe target ((Recipe effect t deps) ': leftoverPot) where
  recipe = undefined

newtype M1 = M1 ()
newtype M2 = M2 ()
newtype M3 = M3 ()
newtype M4 = M4 ()

r1 :: Recipe IO M1 '[M2, M3]
r1 = undefined

r2 :: Recipe IO M2 '[]
r2 = undefined

r3 :: Recipe IO M3 '[M4]
r3 = undefined

r4 :: Recipe IO M4 '[]
r4 = undefined

cookbook1 = r1 .*. r2 .*. r3 .*. r4 .*. HNil

cookbook2 = r3 .*. r4 .*. r2 .*. r1 .*. HNil

c1 = cook cookbook1 :: IO M4
-- c2 = cook cookbook2 :: IO M4

Answer 1

Well, it's saying there's no such instance because there is no such instance. The instance head you're expecting to match does not match.

HasRecipeCase False target ((Recipe effect target deps)      ': leftoverPot)`
HasRecipeCase False M4     ((Recipe IO     M1     '[M2, M3]) ': '[Recipe IO M2 '[], Recipe IO M3 '[M4], Recipe IO M4 '[]]`

Those don't match, because the instance head requires target to be the same type everywhere to match. But you are attempting to use that instance with target as M1 in one location and M4 in another.