INTERNAL ERROR: length of the return type does not equal to the type's arguments count

[L3odr0id]

Derivation fails with error

reflection: INTERNAL ERROR: length of the return type does not equal to the type's arguments count

Reproduce the error

There are 2 files necessary to reproduce the error. It's important that generator signature and derivations task are in different files.

The src/Design.idr:

module Design

import Data.Fin
import Data.Fuel
import Data.Vect

import Test.DepTyCheck.Gen

%default total

namespace FinsList

  public export
  data FinsList : Nat -> Type where
    Nil  : FinsList n
    (::) : Fin n -> FinsList n -> FinsList n

  public export
  (.length) : FinsList n -> Nat
  (.length) []      = 0
  (.length) (x::xs) = S xs.length

public export
data SomeIdx = A | B

public export
data SomeData : SomeIdx -> Type where
  DA : SomeData A
  DB : SomeData B

namespace Container

  public export
  record Container l where
    type  : SomeData l

  public export
  data ContainersList : SomeIdx -> Type where
    Nil  : ContainersList l
    (::) : Container l -> ContainersList l -> ContainersList l

  public export
  (.length) : ContainersList l -> Nat
  (.length) []      = Z
  (.length) (_::ps) = S ps.length

namespace BigContainer

  public export
  record BigContainer l where
    constructor MkBigContainer
    containers : ContainersList l

  public export
  data BigContainersList : SomeIdx -> Type where
    Nil  : BigContainersList l
    (::) : BigContainer l -> BigContainersList l -> BigContainersList l

  public export
  (.length) : BigContainersList l -> Nat
  (.length) []       = Z
  (.length) (_::usl) = S usl.length

namespace ResultType

  public export
  data ResultType : {l : _} -> 
                    (s : BigContainer l) -> 
                    (usl : BigContainersList l) -> 
                    (subUs : FinsList usl.length) -> Type where
    MkDesign : (s : BigContainer l) ->
               {usl : _} ->
               (subUs : FinsList usl.length) ->
               ResultType {l} s usl subUs

  public export
  data ResultTypesList : BigContainersList l -> Type where
    Nil  : ResultTypesList usl
    (::) : {s : _} -> {usl : _} -> {subUs : _} ->
           ResultType {l} s usl subUs -> ResultTypesList {l} (s::usl) -> ResultTypesList {l} usl

export
genResultTypesList : Fuel -> (l : SomeIdx) -> (usl : BigContainersList l) -> Gen MaybeEmpty $ ResultTypesList usl

The src/Derived.idr:

module Derived

import Deriving.DepTyCheck.Gen

import public Design

%default total

%logging "deptycheck" 20

Design.genResultTypesList = deriveGen

The test-project.ipkg:

package test-project

sourcedir = "src"
builddir = ".build"

version = 0.1.0
langversion >= 0.7.0

executable = test-project
main = Derived

depends = collection-utils
        , deptycheck >= 0.0.250305
        , getopts
        , i-hate-parens
        , prettier
        , fin-lizzie

Full derivation log

% pack build
[ info ] Found local config at path
[ info ] Using package collection nightly-260225
[ info ] Building: verilog-model
[ build ] 2/2: Building Derived (src/Derived.idr)
[ build ] LOG deptycheck.derive.namesInfo:10:  ____ start ____
[ build ] LOG deptycheck.derive.namesInfo:10:  ^^^^  end  ^^^^
[ build ] LOG deptycheck.derive.consRec:10:  ____ start ____
[ build ] LOG deptycheck.derive.consRec:12: Design.BigContainer.BigContainer ___ start ___
[ build ] LOG deptycheck.derive.consRec:12: Design.BigContainer.BigContainer ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Design.BigContainer.BigContainersList ___ start ___
[ build ] LOG deptycheck.derive.consRec:7: Design.BigContainer.BigContainersList (::) - directly recursive args: [2]
[ build ] LOG deptycheck.derive.consRec:12: Design.BigContainer.BigContainersList ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Design.Container.Container ___ start ___
[ build ] LOG deptycheck.derive.consRec:12: Design.Container.Container ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Design.Container.ContainersList ___ start ___
[ build ] LOG deptycheck.derive.consRec:7: Design.Container.ContainersList (::) - directly recursive args: [2]
[ build ] LOG deptycheck.derive.consRec:12: Design.Container.ContainersList ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Data.Fin.Fin ___ start ___
[ build ] LOG deptycheck.derive.consRec:7: Data.Fin.Fin FS - directly recursive args: [1]
[ build ] LOG deptycheck.derive.consRec:12: Data.Fin.Fin ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Design.FinsList.FinsList ___ start ___
[ build ] LOG deptycheck.derive.consRec:7: Design.FinsList.FinsList (::) - directly recursive args: [2]
[ build ] LOG deptycheck.derive.consRec:12: Design.FinsList.FinsList ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Prelude.Types.Nat ___ start ___
[ build ] LOG deptycheck.derive.consRec:7: Prelude.Types.Nat S - directly recursive args: [0]
[ build ] LOG deptycheck.derive.consRec:12: Prelude.Types.Nat ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Design.ResultType.ResultType ___ start ___
[ build ] LOG deptycheck.derive.consRec:12: Design.ResultType.ResultType ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Design.ResultType.ResultTypesList ___ start ___
[ build ] LOG deptycheck.derive.consRec:7: Design.ResultType.ResultTypesList (::) - directly recursive args: [5]
[ build ] LOG deptycheck.derive.consRec:12: Design.ResultType.ResultTypesList ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Design.SomeIdx ___ start ___
[ build ] LOG deptycheck.derive.consRec:12: Design.SomeIdx ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:10:  ^^^^  end  ^^^^
[ build ] LOG deptycheck.derive.type:2: Design.ResultType.ResultTypesList[0(l), 1] ___ start ___
[ build ] LOG deptycheck.derive.consBody:2: Design.ResultType.ResultTypesList[0(l), 1] Nil __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.ResultType.ResultTypesList[0(l), 1] Nil - determ: {#0 -> <=[] ->[], #1 (usl) -> <=[] ->[#0]}
[ build ] LOG deptycheck.derive.least-effort:15: Design.ResultType.ResultTypesList[0(l), 1] Nil - givs: [#0, #1 (usl)]
[ build ] LOG deptycheck.derive.least-effort:7: Design.ResultType.ResultTypesList[0(l), 1] Nil - used final order: []
[ build ] LOG deptycheck.derive.consBody:2: Design.ResultType.ResultTypesList[0(l), 1] Nil ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:2: Design.ResultType.ResultTypesList[0(l), 1] (::) __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.ResultType.ResultTypesList[0(l), 1] (::) - determ: {#0 (l) -> <=[] ->[], #1 (s) -> <=[] ->[#0 (l)], #2 (usl) -> <=[] ->[#0 (l)], #3 (subUs) -> <=[#0 (l), #2 (usl)] ->[], #4 -> <=[] ->[#0 (l), #1 (s), #2 (usl), #3 (subUs)], #5 -> <=[#0 (l), #1 (s), #2 (usl)] ->[]}
[ build ] LOG deptycheck.derive.least-effort:15: Design.ResultType.ResultTypesList[0(l), 1] (::) - givs: [#0 (l), #2 (usl)]
[ build ] LOG deptycheck.derive.least-effort:7: Design.ResultType.ResultTypesList[0(l), 1] (::) - used final order: [#4, #5]
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.ResultType.ResultType[0(l), 2(usl)] is used as an internal generator
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.ResultType.ResultTypesList[0(l), 1] is used as an internal generator
[ build ] LOG deptycheck.derive.consBody:2: Design.ResultType.ResultTypesList[0(l), 1] (::) ^^  end  ^^
[ build ] LOG deptycheck.derive.type:2: Design.ResultType.ResultTypesList[0(l), 1] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:2: Design.ResultType.ResultType[0(l), 2(usl)] ___ start ___
[ build ] LOG deptycheck.derive.consBody:2: Design.ResultType.ResultType[0(l), 2(usl)] MkDesign __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.ResultType.ResultType[0(l), 2(usl)] MkDesign - determ: {#0 (l) -> <=[] ->[], #1 (s) -> <=[] ->[#0 (l)], #2 (usl) -> <=[] ->[#0 (l)], #3 (subUs) -> <=[#0 (l), #2 (usl)] ->[]}
[ build ] LOG deptycheck.derive.least-effort:15: Design.ResultType.ResultType[0(l), 2(usl)] MkDesign - givs: [#0 (l), #2 (usl)]
[ build ] LOG deptycheck.derive.least-effort:7: Design.ResultType.ResultType[0(l), 2(usl)] MkDesign - used final order: [#3 (subUs), #1 (s)]
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.FinsList.FinsList[0] is used as an internal generator
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.BigContainer.BigContainer[0(l)] is used as an internal generator
[ build ] LOG deptycheck.derive.consBody:2: Design.ResultType.ResultType[0(l), 2(usl)] MkDesign ^^  end  ^^
[ build ] LOG deptycheck.derive.type:2: Design.ResultType.ResultType[0(l), 2(usl)] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:2: Design.BigContainer.BigContainer[0(l)] ___ start ___
[ build ] LOG deptycheck.derive.consBody:2: Design.BigContainer.BigContainer[0(l)] MkBigContainer __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.BigContainer.BigContainer[0(l)] MkBigContainer - determ: {#0 (l) -> <=[] ->[], #1 (Containers) -> <=[] ->[#0 (l)]}
[ build ] LOG deptycheck.derive.least-effort:15: Design.BigContainer.BigContainer[0(l)] MkBigContainer - givs: [#0 (l)]
[ build ] LOG deptycheck.derive.least-effort:7: Design.BigContainer.BigContainer[0(l)] MkBigContainer - used final order: [#1 (Containers)]
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.Container.ContainersList[0] is used as an internal generator
[ build ] LOG deptycheck.derive.consBody:2: Design.BigContainer.BigContainer[0(l)] MkBigContainer ^^  end  ^^
[ build ] LOG deptycheck.derive.type:2: Design.BigContainer.BigContainer[0(l)] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:2: Design.FinsList.FinsList[0] ___ start ___
[ build ] LOG deptycheck.derive.consBody:2: Design.FinsList.FinsList[0] Nil __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.FinsList.FinsList[0] Nil - determ: {#0 (n) -> <=[] ->[]}
[ build ] LOG deptycheck.derive.least-effort:15: Design.FinsList.FinsList[0] Nil - givs: [#0 (n)]
[ build ] LOG deptycheck.derive.least-effort:7: Design.FinsList.FinsList[0] Nil - used final order: []
[ build ] LOG deptycheck.derive.consBody:2: Design.FinsList.FinsList[0] Nil ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:2: Design.FinsList.FinsList[0] (::) __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.FinsList.FinsList[0] (::) - determ: {#0 (n) -> <=[] ->[], #1 -> <=[] ->[#0 (n)], #2 -> <=[] ->[#0 (n)]}
[ build ] LOG deptycheck.derive.least-effort:15: Design.FinsList.FinsList[0] (::) - givs: [#0 (n)]
[ build ] LOG deptycheck.derive.least-effort:7: Design.FinsList.FinsList[0] (::) - used final order: [#1, #2]
[ build ] LOG deptycheck.derive.closuring.internal:20: Data.Fin.Fin[0(n)] is used as an internal generator
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.FinsList.FinsList[0] is used as an internal generator
[ build ] LOG deptycheck.derive.consBody:2: Design.FinsList.FinsList[0] (::) ^^  end  ^^
[ build ] LOG deptycheck.derive.type:2: Design.FinsList.FinsList[0] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:2: Data.Fin.Fin[0(n)] ___ start ___
[ build ] LOG deptycheck.derive.consBody:2: Data.Fin.Fin[0(n)] FZ __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Data.Fin.Fin[0(n)] FZ - determ: {#0 (k) -> <=[] ->[]}
[ build ] LOG deptycheck.derive.least-effort:15: Data.Fin.Fin[0(n)] FZ - givs: [#0 (k)]
[ build ] LOG deptycheck.derive.least-effort:7: Data.Fin.Fin[0(n)] FZ - used final order: []
[ build ] LOG deptycheck.derive.consBody:2: Data.Fin.Fin[0(n)] FZ ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:2: Data.Fin.Fin[0(n)] FS __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Data.Fin.Fin[0(n)] FS - determ: {#0 (k) -> <=[] ->[], #1 -> <=[] ->[#0 (k)]}
[ build ] LOG deptycheck.derive.least-effort:15: Data.Fin.Fin[0(n)] FS - givs: [#0 (k)]
[ build ] LOG deptycheck.derive.least-effort:7: Data.Fin.Fin[0(n)] FS - used final order: [#1]
[ build ] LOG deptycheck.derive.closuring.internal:20: Data.Fin.Fin[0(n)] is used as an internal generator
[ build ] LOG deptycheck.derive.consBody:2: Data.Fin.Fin[0(n)] FS ^^  end  ^^
[ build ] LOG deptycheck.derive.type:2: Data.Fin.Fin[0(n)] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:2: Design.Container.ContainersList[0] ___ start ___
[ build ] LOG deptycheck.derive.consBody:2: Design.Container.ContainersList[0] Nil __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.Container.ContainersList[0] Nil - determ: {#0 (l) -> <=[] ->[]}
[ build ] LOG deptycheck.derive.least-effort:15: Design.Container.ContainersList[0] Nil - givs: [#0 (l)]
[ build ] LOG deptycheck.derive.least-effort:7: Design.Container.ContainersList[0] Nil - used final order: []
[ build ] LOG deptycheck.derive.consBody:2: Design.Container.ContainersList[0] Nil ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:2: Design.Container.ContainersList[0] (::) __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.Container.ContainersList[0] (::) - determ: {#0 (l) -> <=[] ->[], #1 -> <=[] ->[#0 (l)], #2 -> <=[] ->[#0 (l)]}
[ build ] LOG deptycheck.derive.least-effort:15: Design.Container.ContainersList[0] (::) - givs: [#0 (l)]
[ build ] LOG deptycheck.derive.least-effort:7: Design.Container.ContainersList[0] (::) - used final order: [#1, #2]
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.Container.Container[0(l)] is used as an internal generator
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.Container.ContainersList[0] is used as an internal generator
[ build ] LOG deptycheck.derive.consBody:2: Design.Container.ContainersList[0] (::) ^^  end  ^^
[ build ] LOG deptycheck.derive.type:2: Design.Container.ContainersList[0] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:2: Design.Container.Container[0(l)] ___ start ___
[ build ] LOG deptycheck.derive.consBody:2: Design.Container.Container[0(l)] Container __ start __
[ build ] Error: While processing right hand side of genResultTypesList. Error during
[ build ] reflection: INTERNAL ERROR: length of the return type does not equal to the type's arguments count
[ build ] 
[ build ] Design:35:3--37:23
[ build ] 
[ fatal ] Error when executing system command.

Pack collection used

nightly-260225

[L3odr0id]

It turned out the problem is that no constructor name declared for Container.

Shrinked example

public export
data SomeIdx = A | B

public export
data SomeData : SomeIdx -> Type where
  DA : SomeData A
  DB : SomeData B

public export
record Container l where
  type  : SomeData l

export
genContainer : Fuel -> (l : SomeIdx) -> Gen MaybeEmpty $ Container l

If the generator signature and derivation task are in the same file derivation finishes successfully.

Success log

[ build ] 1/2: Building Design (src/Design.idr)
[ build ] LOG deptycheck.derive.namesInfo:10:  ____ start ____
[ build ] LOG deptycheck.derive.namesInfo:10:  ^^^^  end  ^^^^
[ build ] LOG deptycheck.derive.consRec:10:  ____ start ____
[ build ] LOG deptycheck.derive.consRec:12: Design.Container ___ start ___
[ build ] LOG deptycheck.derive.consRec:12: Design.Container ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Design.SomeData ___ start ___
[ build ] LOG deptycheck.derive.consRec:12: Design.SomeData ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:12: Design.SomeIdx ___ start ___
[ build ] LOG deptycheck.derive.consRec:12: Design.SomeIdx ^^^  end  ^^^
[ build ] LOG deptycheck.derive.consRec:10:  ^^^^  end  ^^^^
[ build ] LOG deptycheck.derive.type:2: Design.Container[0(l)] ___ start ___
[ build ] LOG deptycheck.derive.consBody:2: Design.Container[0(l)] Container __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.Container[0(l)] Container - determ: {#0 (l) -> <=[] ->[], #1 (type) -> <=[] ->[#0 (l)]}
[ build ] LOG deptycheck.derive.least-effort:15: Design.Container[0(l)] Container - givs: [#0 (l)]
[ build ] LOG deptycheck.derive.least-effort:7: Design.Container[0(l)] Container - used final order: [#1 (type)]
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.SomeData[0] is used as an internal generator
[ build ] LOG deptycheck.derive.consBody:2: Design.Container[0(l)] Container ^^  end  ^^
[ build ] LOG deptycheck.derive.type:2: Design.Container[0(l)] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:2: Design.SomeData[0] ___ start ___
[ build ] LOG deptycheck.derive.consBody:2: Design.SomeData[0] DA __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.SomeData[0] DA - determ: {}
[ build ] LOG deptycheck.derive.least-effort:15: Design.SomeData[0] DA - givs: []
[ build ] LOG deptycheck.derive.least-effort:7: Design.SomeData[0] DA - used final order: []
[ build ] LOG deptycheck.derive.consBody:2: Design.SomeData[0] DA ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:2: Design.SomeData[0] DB __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Design.SomeData[0] DB - determ: {}
[ build ] LOG deptycheck.derive.least-effort:15: Design.SomeData[0] DB - givs: []
[ build ] LOG deptycheck.derive.least-effort:7: Design.SomeData[0] DB - used final order: []
[ build ] LOG deptycheck.derive.consBody:2: Design.SomeData[0] DB ^^  end  ^^
[ build ] LOG deptycheck.derive.type:2: Design.SomeData[0] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.closuring.internal:20: Design.Container[0(l)] is used as an internal generator

[buzden]

It looks like a problem in the compiler with DN names, since consturctor's name is a NS .. $ DN "Rec" $ MN "__mkRec" 0...

[buzden]

This is related to idris-lang/Idris2#3532