I'm currently experimenting with typelevel code. I've got one instance with a type variable that only occurs in the context, and not in the instance itself. Somehow the compiler doesn't like that, but I can't figure out why not. Adding a functional dependency to HasRecipe
effect pot target -> deps
works for that error, but then the incorrect deps
are inferred at the test in the last line of the code.
Error:
• Could not deduce (HasRecipe target pot effect deps0)
from the context: (HasRecipe target pot effect deps,
SubSelect pot deps)
bound by an instance declaration:
forall target (pot :: [*]) (effect :: * -> *) (deps :: [*]).
(HasRecipe target pot effect deps, SubSelect pot deps) =>
CanCook target pot effect
at Lib.hs:15:10-92
The type variable ‘deps0’ is ambiguous
• In the ambiguity check for an instance declaration
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the instance declaration for ‘CanCook target pot effect’
Source:
#!/usr/bin/env stack
-- stack --resolver lts-11.4 --install-ghc runghc
{-# 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
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 CanCook target (pot :: [*]) effect | pot -> effect where
cook :: HList pot -> effect target
instance (HasRecipe target pot effect deps, SubSelect pot deps) => CanCook target pot effect where
cook pot =
let
deps :: HList deps
deps = subselect pot
r :: Recipe effect target deps
r = recipe pot
in
runRecipe r $ deps
type family PotEffect (pot :: [*]) where
PotEffect (Recipe effect _ _ ': '[]) = effect
PotEffect (Recipe effect _ _ ': tail) = effect
class HasRecipe target (pot :: [*]) effect deps | pot -> effect where
recipe :: HList pot -> Recipe effect target deps
class SubSelect (pot :: [*]) (deps :: [*]) where
subselect :: HList pot -> HList deps
instance SubSelect t f where
subselect = undefined
class HasRecipeCase (b :: Bool) (target :: *) (pot :: [*]) effect (deps :: [*]) | pot -> effect where
recipeCase :: Proxy b -> Proxy target -> HList pot -> Recipe effect target deps
instance HasRecipeCase True target ((Recipe effect target deps) ': leftoverPot) effect deps where
recipeCase _ _ (HCons head _) = head
instance (HasRecipe target leftoverPot effect deps) =>
HasRecipeCase False target ((Recipe effect target1 deps) ': leftoverPot) effect deps where
recipeCase _ _ (HCons _ tail) = recipe tail
instance (HEq target t bool, HasRecipeCase bool target pot effect deps, pot ~ ((Recipe effect t deps) ': leftoverPot)) =>
HasRecipe target ((Recipe effect t deps) ': leftoverPot) effect deps 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