На моей (по общему признанию, замученной) функции Haskell появляется ложное ограничение. Как я могу удовлетворить это?

Question

Играя с DataKinds в Haskell я создал следующий код, который реализует и использует некоторые унарные nats на уровне типов:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Demo where
import Data.Proxy
import Data.Semigroup
import Numeric.Natural
import Data.Constraint

data Nat = Zero | Succ Nat

type family Pred (n :: Nat) where Pred ('Succ n) = n

class IsNat (n :: Nat) where
  nat :: proxy n -> Natural
  unNat :: proxy n -> (n ~ 'Zero => x) -> ((n ~ 'Succ (Pred n), IsNat (Pred n)) => x) -> x

instance IsNat 'Zero where
  nat _ = 0
  unNat _ z _ = z

instance IsNat n => IsNat ('Succ n) where
  nat _ = succ (nat (Proxy @n))
  unNat _ _ s = s

noneIsNotSuccd :: (n ~ 'Zero, n ~ 'Succ (Pred n)) => proxy n -> a
noneIsNotSuccd _ = error "GHC proved ('Zero ~ 'Succ (Pred 'Zero))!"  -- don't worry, this won't happen

predSuccIsNat :: forall n proxy r. (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r

data Indexed (n :: Nat) where
  Z :: Indexed 'Zero
  S :: Indexed n -> Indexed ('Succ n)

instance Show (Indexed n) where
  show Z = "0"
  show (S n) = "S" <> show n

recr :: forall n x. (IsNat n, Semigroup x) => (forall k. IsNat k => Indexed k -> x) -> Indexed n -> x
recr f Z = f Z
recr f (S predn) = predSuccIsNat (Proxy @n) (f predn) <> f (S predn)

main :: IO ()
main = print $ getSum $ recr (Sum . nat) (S Z)

Когда я пытаюсь скомпилировать его в GHC 8.2.2, я получаю следующую ошибку типа:

Demo.hs:35:25: error:
    • Could not deduce (IsNat (Pred n)) arising from a use of ‘unNat’
      from the context: n ~ 'Succ (Pred n)
        bound by the type signature for:
                   predSuccIsNat :: forall (n :: Nat) (proxy :: Nat -> *) r.
                                    n ~ 'Succ (Pred n) =>
                                    proxy n -> (IsNat (Pred n) => r) -> r
        at Demo.hs:34:1-96
    • In the expression: unNat proxy (noneIsNotSuccd proxy) r
      In an equation for ‘predSuccIsNat’:
          predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
   |
35 | predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
   |                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

По общему признанию, это улучшение по сравнению с тем, что происходит в GHC 8.0.1, где он прекрасно компилируется и затем завершается с ошибкой во время выполнения:

*** Exception: Demo.hs:34:23: error:
    • Could not deduce (IsNat (Pred n)) arising from a use of ‘unNat’
      from the context: n ~ 'Succ (Pred n)
        bound by the type signature for:
                   predSuccIsNat :: n ~ 'Succ (Pred n) =>
                                    proxy n -> (IsNat (Pred n) => r) -> r
        at Demo.hs:33:1-78
    • In the expression: unNat proxy (noneIsNotSuccd proxy)
      In an equation for ‘predSuccIsNat’:
          predSuccIsNat proxy = unNat proxy (noneIsNotSuccd proxy)
(deferred type error)

Похоже, что в GHC 8.2.2, unNat принимает неявное (IsNat (Pred n)) ограничение, которое не отображается в сигнатуре типа:

λ» :t unNat
unNat
  :: IsNat n =>
     proxy n
     -> (n ~ 'Zero => x)
     -> ((n ~ 'Succ (Pred n), IsNat (Pred n)) => x)
     -> x

Можно ли мне позвонить unNat реализовать что-то вроде predSuccIsNat?

Answer 1

predSuccIsNat :: forall n proxy r. (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
                        ^^^^^

Я не знаю, где вы ожидаете получить IsNat словарь, который вам нужен для того, чтобы использовать unNat, Если я добавлю его в подпись типа

predSuccIsNat :: forall n proxy r. IsNat n => (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r

все работает нормально (на ghc 8.2.1, которая имеет ту же проблему с отложенным вызовом, что и 8.0.1).

Без этого кажется, что вы хотите сделать вывод, что если n ~ 'Succ (Pred n) затем IsNat n - предположительно из-за того, что Pred n определяется только на Succs. Но даже если сделать такой вывод, этого будет недостаточно. Например n ~ Succ m недостаточно, чтобы вывести IsNat либо вам также понадобится IsNat m,