Infer ограничения семейств типа с ограничениями аргументов

Question

У меня есть куча сложных функций уровня типа, оценивающих на такие вещи, как:

(If (EqNat n 2) 
    1 
    (If (EqNat n 1) 
    2 
    (If (EqNat n 0) 3 0))) 

Теперь, очевидно, в данном случае это выражение является KnownNat. Больше в целом мы можем сказать:

forall (c :: * -> Constraint) (p :: Bool) a b . 
(c a, c b) => c (If p a b) 

Есть ли способ, чтобы научить GHC вывести это?

Edit: @chi отметил, что в некоторых случаях это разрешимо GADTs но мой частный случай это один:

module M1 (C(..)) where 

type familiy NestedIfs (n :: Nat) :: Nat 
type NestedIfs n = <<complex nested ifs like the above that evals to literals>> 

class C a (n :: Nat) where 
    f :: KnownNat n => a -> NestedIfs n -> Bool 

, а затем

module M2() where 
import M1 

instance C Int n where 
    f = ...require that KnownNat (NestedIfs n)... 

NestedIfs не доступен для M2 но возможно, GHC должен иметь возможность заключить, что forall n . KnownNat n => KnownNat (NestedIfs n) от общий вывод Я упоминал выше.

Answer 1

Этот вопрос не является сложным, но является некорректным. Какую ценность вы ожидаете получить от типа c (If p a b) :: Constraint? То, что вы, вероятно, хотите спросить, как заполнить в теле этого

bisect :: forall b c x y. SingI b => Proxy b -> (c x, c y) :- c (If b x y) 

Здесь, как было отмечено в комментариях, я принуждая c быть синглтон, так что я могу получить Either (c :~: True) (c :~: False) (вы можете прочитать мой Что c :: Bool должно быть True или False, что, к сожалению, нет, это тривиальный запрос, когда на уровне типа с Any есть вид Bool). :- поставляется с пакетом constraints. Это способ сказать, что ограничение (a,b) подразумевает ограничение If c a b. То есть точно как выразить свой запрос - вы хотите подтверждение, что два говорит данным c x и c y hold, c (If b x y) также будет содержать.

Наполнитель в теле этой функции на самом деле очень мало код:

{-# LANGUAGE DataKinds, TypeFamilies, ConstraintKinds, TypeOperators, RankNTypes, 
    ScopedTypeVariables, PolyKinds #-} 

import Data.Constraint 
import Data.Singletons.Prelude hiding ((:-)) 

bisect :: forall b c x y. (SingI b) => Proxy b -> (c x, c y) :- c (If b x y) 
bisect _ = unmapDict $ case sing :: Sing b of 
         STrue -> mapDict weaken1 
         SFalse -> mapDict weaken2