Generate type class constraints recursively and use them in a recursive function

Question

I am trying to define a function which gets some natural number n as input. Depending on this input the function should have different constraints. This constraints get calculate with a type family. The number has to be converted to GHC.TypeNats because the constraints are for Data.Vector.Sized. I asked a similar question here, but the answer won't work in the case of GHC.TypeNats and arbitrary n.

I tried the UNat type from Clash.

This is the relevant code from clash:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE Trustworthy #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}


import GHC.TypeNats
import GHC.Natural

import Unsafe.Coerce      (unsafeCoerce)
import Data.Kind (Constraint)

data SNat (n :: Nat) where
  SNat :: KnownNat n => SNat n

data UNat :: Nat -> * where
  UZero :: UNat 0
  USucc :: UNat n -> UNat (n + 1)

snatToInteger :: SNat n -> Natural
snatToInteger p@SNat = natVal p

toUNat :: forall n. SNat n -> UNat n
toUNat p@SNat = fromI @n (snatToInteger p)
  where
    fromI :: forall m. Natural -> UNat m
    fromI 0 = unsafeCoerce @(UNat 0) @(UNat m) UZero
    fromI n = unsafeCoerce @(UNat ((m-1)+1)) @(UNat m) (USucc (fromI @(m-1) (n - 1)))

This solves the problem with recursion, but not with constraints.

Here is a minimal example:

type family F (m :: Nat) (n :: Nat) :: Constraint where
  F m 0 = ()
  F m n = ((0 <=? m) ~ 'True, F m (n - 1))

fU :: forall m n. (KnownNat m, KnownNat n, F m n) => UNat n -> ()
fU UZero = ()
fU (USucc s) = fU @m s

This gives back the error:

• Could not deduce: F m n1 arising from a use of ‘fU’
      from the context: (KnownNat m, KnownNat n, F m n)
        bound by the type signature for:
                   fU :: forall (m :: Nat) (n :: Nat).
                         (KnownNat m, KnownNat n, F m n) =>
                         UNat n -> ()
        at src-lib/Anomaly/NeuralNetworks/Peano.hs:103:1-65
      or from: n ~ (n1 + 1)
        bound by a pattern with constructor:
                   USucc :: forall (n :: Nat). UNat n -> UNat (n + 1),
                 in an equation for ‘fU’
        at src-lib/Anomaly/NeuralNetworks/Peano.hs:105:5-11
    • In the expression: fU @m s
      In an equation for ‘fU’: fU (USucc s) = fU @m s
    • Relevant bindings include
        s :: UNat n1
          (bound at src-lib/Anomaly/NeuralNetworks/Peano.hs:105:11)
    |
105 | fU (USucc s) = fU @m s
    |                ^^^^^^^

StillerHarpo StillerHarpo · Accepted Answer · 2020-12-08T08:19:07

I solved this by adding the constraints to the construtors of the GADT Peano nat.

data CNat :: Nat -> Nat -> * where
  CZero :: forall n m. CNat 0 m
  CSucc :: forall n m. (0 <=? m) ~ 'True => CNat n m -> CNat (n + 1) m

fC :: forall n m. (KnownNat n, KnownNat m) => CNat n m -> ()
fC CZero = ()
fC (CSucc s) = fC s

Here is an example which shows that the condition really holds in the second pattern.

hC :: forall m. ((0 <=? m) ~ 'True) => ()
hC = ()

gC :: forall n m. CNat n m -> () -> ()
gC CZero _ = ()
gC (CSucc s) _ = gC s (hC @m)

Generate type class constraints recursively and use them in a recursive function

1 Answers