为什么在使用 Bool 和 Finite 2 时出现非详尽模式警告？

Question

我希望通过 Finite 2 为 Bool 定义一个新 class 的实例，而不创建部分函数，但它不起作用。

我的代码：

-- SO test case, re: my HasFin instance for Bool.
--
-- David Banas <capn.freako@gmail.com>
-- February 9, 2018

{-# OPTIONS_GHC -Wall #-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}

module Bogus.BoolHasFin where

import GHC.TypeLits
import Data.Finite
import Data.Finite.Internal (Finite(..))

class KnownNat (Card a) => HasFin a where
  type Card a :: Nat
  toFin :: a -> Finite (Card a)
  unFin :: Finite (Card a) -> a

instance HasFin Bool where
  type Card Bool = 2

  toFin False = finite 0
  toFin True  = finite 1

  unFin = \case
    Finite 0 -> False
    Finite 1 -> True

以及GHC编译结果：

Davids-Air-2:test dbanas$ stack ghc -- -c so_BoolHasFin.hs 

so_BoolHasFin.hs:30:11: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative:
        Patterns not matched: (Finite p) where p is not one of {1, 0}

任何人都可以帮助我理解为什么我会收到此警告吗？看起来，通过 Finite 2 将参数限制在 unFin 应该就足够了。

添加于 2018-02-10：

根据 Conal 私下提出的建议，此代码：

unFin (Finite 0) = False
unFin _          = True

消除警告。

Answer 1

我认为这至少部分是因为 Finite 的定义中没有任何内容将包含的 Integer 限制在假定范围内（0 到 n-1): newtype Finite (n :: Nat) = Finite Integer.

为什么在使用 Bool 和 Finite 2 时出现非详尽模式警告？

Why non-exhaustive patterns warning, when using Bool and Finite 2?

haskell

types

ghc