前のNatのSingIを推論できません

Question

私は有限の整数セットのためにweaken関数を書こうとしています。私はsingletonsパッケージを使用しています。私は、加算、減算、および前の関数を定義し、昇格させただけでなく、型チェッカーの助けとなるいくつかの式を証明しました。しかし、私が得ているエラーは、すべてのこととはまったく無関係です。

weaken :: forall n m k . (SingI n, SingI m, SingI k, (Minus m n) ~ NatJust k) => Fin n -> Fin m 
weaken ZF = gcastWith (apply Refl $ plus_minus sm sn sk) ZF 
    where sn = sing :: SNat n 
     sm = sing :: SNat m 
     sk = sing :: SNat k 
weaken (SF n) = gcastWith (apply Refl $ succ_pred sm) (SF (weaken n)) 
    where sn = sing :: SNat n 
     sm = sing :: SNat m 
     sk = sing :: SNat k 

私は取得していますエラーがweaken（SF (weaken n)）の再帰呼び出しであると次のようである：n1が正しくタイプnのタイプレベルの前任者であることを推測さCould not deduce (SingI n1)、。 I SingI (Pred n)という制約を追加することはできますが、これは問題を1レベル下に移動するだけです（GHCは(SingI (Pred (Pred n)))の相当量を推測できないと言っています）。

SingI (Pred n)がSingI nに続くことをGHCに納得させるにはどうすればよいですか（なぜsingletonsパッケージではこれが既に行われていますか）。

Answer 1

GHC.TypeLitsは、最終的にはタイプレベルで非負のInteger -sを提供し、シングルトンランタイム操作を実行する関数をエクスポートしません。例えば、KnownNat aとKnownNat bを指定すると、実行時にKnownNat (a + b)を生成する標準関数はありません。

singletonsは、singleton Nat operationsを安全に実装することでこれを解決します。

singletons減算機能は、否定的な結果のためにエラーがスローされます（そして、私たちが望むだろうと0に切り捨てられません）ので、私たちはpredのためにそれを再利用し、それを自分自身を実装することはできません。

{-# language TypeApplications #-} -- plus all the usual exts 

import Data.Singletons.Prelude 
import Data.Singletons.TypeLits 
import Unsafe.Coerce 

type family Pred (n :: Nat) :: Nat where 
    Pred 0 = 0 
    Pred n = n :- 1 

sPred :: Sing n -> Sing (Pred n) 
sPred sn = case fromSing sn of 
    0 -> unsafeCoerce (sing @_ @0) 
    n -> case toSing @Nat (n - 1) of 
    SomeSing sn -> unsafeCoerce sn 

sPredを使用してを取得し、次にwithSingIまたはsingInstanceを入力してSingI (Pred n)に変換することができます。

SingIはweakenには使用しないでください。 SingIの目的は、シングルトンパラメータを他の関数に転送する以外には使用しないコンテキストで自動的にプラグインすることです。代わりにSingを使用すると、singを避けてアノテーションノイズを入力することができます。私の経験では、singletonsプログラミングの時間の約90％でSingIよりもSingが好ましい。