上下文中的类型变量不固定？ [英] Type variables in context not fixed?

问题描述

我目前正在尝试使用typelevel代码。我有一个只有上下文中出现的类型变量的实例，而不是实例本身。不知何故，编译器不喜欢这一点，但我不明白为什么不。将函数依赖项添加到 HasRecipe effect pot target - > deps 适用于该错误，但在代码最后一行的测试中推断不正确的 deps 。

错误：

 •无法推断（HasRecipe目标罐效应deps0）
从上下文：（HasRecipe目标锅效果deps，
 SubSelect罐deps）
由实例声明：
 forall目标（pot :: [*]）（效果:: *  - > ; *）（deps :: [*]）。 
（HasRecipe目标罐效果缩放，SubSelect罐缩放）=> 
 CanCook在Lib.hs：15：10-92处获得
 
类型变量'deps0'不明确
•在对实例声明$ b $进行歧义检查时b要推迟歧义检查以使用站点，请启用AllowAmbiguousTypes 
在'CanCook目标锅效应'的实例声明中
  

来源：

 ＃！/ usr / bin / env堆栈
  - 堆栈 - 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数据实例HList（l :: [*]）
 
数据实例HList'[] = HNil 
数据实例HList（x'：xs）= x'HCons` HList xs 
 
导出实例Eq（HList'[]）
导出实例（Eq x，Eq（HList xs））=>等式（HList（x'：xs））
 
导出实例Ord（HList'[]）
导出实例（Ord x，Ord（HList xs））=> Ord（HList（x'：xs））
 
导出实例有界（HList'[]）
导出实例（有界x，有界（HList xs））=>有界的（HList（x'：xs））
 
 class HExtend e l其中
 type HExtendR e l 
（。*。）:: e  - > l  - > HExtendR e l 
 
 infixr 2。*。 
 
实例HExtend e（HList l）其中
 type HExtendR e（HList l）= HList（e'：l）
（。*。）= HCons 
 
 
 main = pure（）
 
 newtype配方效果目标（deps :: [*]）=配方{runRecipe :: HList deps  - >效果目标} 
 
类CanCook目标（pot :: [*]）效果|锅 - >效果
 cook :: HList pot  - >效果目标
 
实例（HasRecipe目标罐效果缩放，SubSelect罐缩放）=> CanCook目标锅效应，其中
 cook pot = 
 let 
 deps :: HList deps 
 deps = subselect pot 
r :: Recipe effect target deps 
r = recipe pot 
 in 
 runRecipe r $ deps 
 
类型PotEffect（pot :: [*]）其中
 PotEffect（Recipe effect _ _'：'[]） =效果
 PotEffect（食谱效果_ _'：尾巴）=效果
 
类HasRecipe目标（pot :: [*]）效果deps |锅 - >效果其中
 recipe :: HList pot  - >配方效果目标代价
 
 class SubSelect（pot :: [*]）（deps :: [*]）其中
 subselect :: HList pot  - > HList deps 
 
实例SubSelect tf其中
 subselect = undefined 
 
类HasRecipeCase（b :: Bool）（target :: *）（pot :: [*] ）效果（deps :: [*]）|锅 - >效果其中
 recipeCase :: Proxy b  - >代理目标 - > HList罐 - > 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 ::配方IO M1'[M2，M3] 
 r1 =未定义
 
 r2 ::配方IO M2'[] 
 r2 =未定义
 
 r3 ::配方IO M3'[M4] 
 r3 =未定义
 
 r4 ::食谱IO M4'[] 
 r4 =未定义
 
 cookbook1 = r1。*。 r2。*。 r3。*。 r4。*。 HNil 
 
 cookbook2 = r3。*。 r4。*。 r2。*。 r1。*。 HNil 
 
 c1 = cook cookbook1 :: IO M4 
  -  c2 = cook cookbook2 :: IO M4 
  

解决方案

您不能拥有像这样的实例

  instance（HasRecipe target pot effect deps，SubSelect pot deps）
 => CanCook目标罐效应，其中
  

tyvar deps 出现在上下文中，但不在头部，使实例变得模糊。

具体而言，可能有四个实例

 实例HasRecipe目标锅效果A 
实例SubSelect锅A 
实例HasRecipe目标锅效果B 
实例SubSelect锅B 
  

和GHC无法选择您想要的。您必须在 cook 呼叫站点上选择 deps 实例定义或（启用不明确的类型） p>

如果有一个fundep，比如 target pot effect - > deps 这将消除歧义，但我很难理解其意图。

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

解决方案

You can't have an instance like this

instance (HasRecipe target pot effect deps, SubSelect pot deps)
       => CanCook target pot effect where

The tyvar deps appears in the context, but not in the head, making the instance ambiguous.

Concretely, it could be possible to have four instances

instance HasRecipe target pot effect A
instance SubSelect pot A
instance HasRecipe target pot effect B
instance SubSelect pot B

and GHC has no way to select which one you want. You have to choose deps either at instance definition, or (enabling ambiguous types) at the cook call site.

If there were a fundep such as target pot effect -> deps this would remove the ambiguity, but it is hard for me to understand the intent.

这篇关于上下文中的类型变量不固定？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！