could not deduce KnownNat

[pieter-bos]

If I submit this program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=500 #-}

module Mod where

import Clash.Prelude

data Sections
  = EmptySections
  | ConsSections Nat Sections

data Rom (z :: Sections) where
  RomNil :: Rom EmptySections
  RomCons ::
    forall (n :: Nat) (z :: Sections) . KnownNat n =>
    BitVector n ->
    Rom z ->
    Rom (ConsSections n z)

type family Length (z :: Sections) where
  Length EmptySections = 0
  Length (ConsSections n z) = n + Length z

blob ::
  forall (z :: Sections) . KnownNat (Length z) =>
  Rom z ->
  BitVector (Length z)
blob RomNil = 0
blob (RomCons section sections) = section ++# (blob sections)

I get:

Repro.hs:1:1: error: [GHC-95822]
    solveWanteds: too many iterations (limit = 500)
      Unsolved: WC {wc_simple =
                      [W] $dKnownNat_a48X {0}:: KnownNat (Length z) (CNonCanonical)}
      Simples: {[W] $dKnownNat_a3Rp {0}:: KnownNat m0 (CNonCanonical),
                [W] hole{co_a3Rr} {0}:: (n0 + m0) ~ Length z (CNonCanonical),
                [W] $dKnownNat_a3Ru {0}:: KnownNat (Length z0) (CNonCanonical),
                [W] hole{co_a3Rw} {0}:: Length z0 ~ m0 (CNonCanonical)}
    Suggested fix:
      Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
  |
1 | {-# LANGUAGE GADTs #-}
  | ^

This comes from the use of blob sections which asks for KnownNat (Length z1) - z1 being the parameter in sections :: Rom z1. Run without the plugins:

Repro.hs:38:43: error: [GHC-39999]
    • Could not deduce ‘KnownNat (Length z1)’
        arising from a use of ‘++#’
      from the context: KnownNat (Length z)
        bound by the type signature for:
                   blob :: forall (z :: Sections).
                           KnownNat (Length z) =>
                           Rom z -> BitVector (Length z)
        at Repro.hs:(33,1)-(36,22)
      or from: (z ~ ConsSections n z1, KnownNat n)
        bound by a pattern with constructor:
                   RomCons :: forall (n :: Nat) (z :: Sections).
                              KnownNat n =>
                              BitVector n -> Rom z -> Rom (ConsSections n z),
                 in an equation for ‘blob’
        at Repro.hs:38:7-30
    • In the expression: section ++# (blob sections)
      In an equation for ‘blob’:
          blob (RomCons section sections) = section ++# (blob sections)
   |
38 | blob (RomCons section sections) = section ++# (blob sections)
   |                                           ^^^

I would expect this to work, since we know z ~ ConsSections n z1 and could obtain Length (ConsSections n z1) = n + Length z1, so from KnownNat (Length z) and KnownNat n I would expect to obtain KnownNat (Length z1).

Christiaan showed me this workaround using subSNat, which does compile:

blob (RomCons @n section sections) =
  case subSNat (SNat @(Length z)) (SNat @n) of
    (SNat :: SNat l1) -> section ++# (blob sections)

Apologies for the less than stellar title, I don't really understand the structure of the problem...