Арифмои и фантомные типы

Question

Я пытаюсь понять использование фантомных типов в пакете arithmoi (https://hackage.haskell.org/package/arithmoi-0.8.0.0).. Это помогает проверить, работаю ли я с правильным классом остатков (Z/nZ).

Тип фантома, о котором идет речь, - data Mod (n :: Nat) = Mod Natural, и, как я понимаю, конструктор не экспортируется. Но конструктор SomeMod экспортируется, поэтому я решил, что должен использовать его для создания переменной ::Mod n. Более того, можно читать в документации, но я не могу ее использовать.

case modulo n m of
  SomeMod k -> process k -- Here k has type Mod m
  InfMod{}  -> error "impossible"

Итак, я попытался:

foo :: KnownNat m => Nat -> Nat -> Mod m
foo n m = case modulo n m of
    (SomeMod k) -> k
    otherwise -> error "some error"

Я получил ошибку о переменной m, m1, которая выходит за пределы области видимости. Я немного озадачен.

Answer 1

Как и IO, экзистенциалы не могут быть экранированы.Однажды в экзистенциальном, всегда в экзистенциальном.Но это нормально - если вы готовы признать KnownNat m, что, как утверждает ваша сигнатура типа, вы готовы сделать, то вы можете просто поднять непосредственно к этому типу.

foo :: KnownNat m => Natural -> Mod m
foo = fromIntegral