小编has*_*eat的帖子

这是 Kattis 提出的一个非常标准的背包问题。下面是 Haskell 中一个简单的动态编程解决方案：

{-# Language OverloadedStrings #-}

import Control.Arrow ((>>>))
import Data.List (intercalate)
import Data.Array
import Data.Maybe
import qualified Data.ByteString.Lazy.Char8 as C

main = C.interact solve

solve = C.words >>> fmap readInt >>> divideInput
        >>> fmap (solveCase >>> toBS)
        >>> C.unlines
  where readInt = C.readInt >>> fromJust >>> fst

divideInput :: [Int] -> [[Int]]
divideInput [] = []
divideInput (c:n:ls) = (c : n : this) : divideInput that
  where (this, that) = splitAt (2*n) ls …

以下代码在 Idris2 中可以正常编译：

C : Nat
C = 2

claim : C = 2
claim = Refl

C但如果不大写则失败：

c : Nat
c = 2

claim : c = 2
claim = Refl

错误信息是

警告：我们将隐式绑定以下小写名称。您可能无意中隐藏了关联的全局定义：c isshadowing Main.c 错误：在处理声明的右侧时。统一时：2 = 2 和：c = 2 不匹配：2 和 c。

有没有办法告诉 Idris 编译器不要隐藏类型中的小写全局名称？

以下代码无法编译:

import Data.Bits
xor2 = xor

但是,一旦我添加了类型信息,它就会编译:

import Data.Bits
xor2 :: Bits a => a->a->a
xor2 = xor

我无法解释这一点.有什么解释吗？