Нормализация неравенств TypeNats

У меня есть две функции, обе с видом Nat (от TypeNats), которые имеют оператор типа сравнения <=. Ограничение 2 <= n для функции b содержит ограничение 1 <= n для функции a. Есть ли способ заставить ghc решить, что 2 <= n удовлетворяет ограничению 1 <= n, чтобы мне не нужно было указывать оба ограничения (1 <= n, 2 <= n) для b?

Код ниже демонстрирует ошибку.

{-# LANGUAGE KindSignatures, TypeOperators, ScopedTypeVariables, 
             DataKinds, TypeFamilies #-}

import GHC.TypeNats
import Data.Proxy

a :: forall (a :: Nat). 1 <= a => Proxy a -> Int
a = undefined

b :: forall (a :: Nat). 2 <= a => Proxy a -> Int
b = a

Выдает ошибку компиляции

• Could not deduce: (1 <=? a) ~ 'True arising from a use of ‘a’
  from the context: 2 <= a
    bound by the type signature for:
               b :: forall (a :: Nat). (2 <= a) => Proxy a -> Int
    at Example.hs:9:1-48
• In the expression: a
  In an equation for ‘b’: b = a
• Relevant bindings include
    b :: Proxy a -> Int
      (bound at Example.hs:10:1)

Существует библиотека для решения равенств ghc-typelits-natnormalise, но не для решения неравенств.


types haskell data-kinds
person William Rusnack    schedule 30.03.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Несмотря на описание пакета, ghc-typelits-natnormalise также может решать неравенства. Следующие программы проверяют тип с помощью GHC 8.6.4 и ghc-typelits-natnormalise-0.6.2:

{-# LANGUAGE KindSignatures, TypeOperators, ScopedTypeVariables,
             DataKinds, TypeFamilies #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -Wall #-}

import GHC.TypeNats
import Data.Proxy

a :: forall (a :: Nat). 1 <= a => Proxy a -> Int
a = undefined

b :: forall (a :: Nat). 2 <= a => Proxy a -> Int
b = a
person K. A. Buhr    schedule 31.03.2019