Infer constraints of type families from constraints of arguments

I have a bunch of complicated type level functions that evaluate to things like:

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

Now obviously in this case this expression is a KnownNat . More generally we may say:

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

Is there a way to teach GHC to infer this?

Edit: @chi noted that in some cases this is solvable with GADTs but my particular case is this one:

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

and then

module M2 () where
import M1

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

NestedIfs is not accessible to M2 but maybe GHC should be able to infer that forall n . KnownNat n => KnownNat (NestedIfs n) forall n . KnownNat n => KnownNat (NestedIfs n) from the general inference I mention above.

---

This question is not hard, but is ill-posed. What value do you expect to get back of type c (If pab) :: Constraint ? What you likely want to ask, is how to fill in the body of this

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

Here, as noted in the comments, I am forcing c to be a singleton so that I can get Either (c :~: True) (c :~: False) (you may read my SingI constraint as enforcing that c :: Bool must be either True or False , which is unfortunately not a trivial request when at the type level since Any has kind Bool too). The :- comes from the constraints package. It is a way of saying that the constraint (a,b) implies the constraint If cab . That is exactly how to express your request - you want a proof that two says given cx and cy hold, c (If bxy) will also hold .

Filling in the body of that function is actually very little code:

{-# 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

链接地址: http://www.djcxy.com/p/7464.html

上一篇: Typescript：函数参数签名的泛型类型

下一篇: 从参数的约束推断类型族的约束