Type mismatch due to lack of reduction of type defined in the same mutual block as target function.

[JadenGeller]

Steps to Reproduce

Compile the following program:

%hide Nat
%hide Nat.S
%hide Nat.Z

function : List Type -> Type -> Type
function [] b = b
function (a :: as) b = a -> function as b

infixr 10 *->

(*->) : List Type -> Type -> Type
(*->) = function

tuple : List Type -> Type
tuple [] = ()
tuple (a :: as) = (a, tuple as)

map : (a -> b) -> (args *-> a) -> (args *-> b)
map f {args=[]}        z = f z
map f {args=(a :: as)} g = \x => map f (g x)

tupleConstructor : (args : List Type) -> args *-> (tuple args)
tupleConstructor [] = ()
tupleConstructor (a :: as) = \x => map (\xs => (x, xs)) (tupleConstructor as)

tupleEliminator : tuple args -> (args *-> a) -> a
tupleEliminator {args=[]}        ()      z = z
tupleEliminator {args=(a :: as)} (x, xs) g = tupleEliminator xs (g x)

--

%auto_implicits off 
record AlgebraicData (Tag : Type) (Payload : Tag -> List Type) where
    constructor MkAlgebraicDataRaw
    tag : Tag
    payload : tuple (Payload tag)
%auto_implicits on 

MkAlgebraicData : {Tag : _, Payload : _} -> (tag : Tag) -> Payload tag *-> AlgebraicData Tag Payload
MkAlgebraicData tag {Payload} = map (MkAlgebraicDataRaw tag) (tupleConstructor (Payload tag))

elimAlgebraicData : {Tag : _, Payload : _} -> ((tag : Tag) -> Payload tag *-> a) -> AlgebraicData Tag Payload  -> a
elimAlgebraicData eliminator (MkAlgebraicDataRaw tag payload) = tupleEliminator payload (eliminator tag)

--

mutual
    data NatTag = Z | S

    NatPayload : NatTag -> List Type
    NatPayload Z = []
    NatPayload S = [Nat]

    Nat : Type
    Nat = AlgebraicData NatTag NatPayload
    
    MkNat : (tag : NatTag) -> NatPayload tag *-> Nat
    MkNat = MkAlgebraicData
    
    elimNat : ((tag : NatTag) -> NatPayload tag *-> a) -> Nat -> a
    elimNat = elimAlgebraicData

zero : Nat
zero = MkNat Z

Expected Behavior

The program type checks because MkNat Z has type function (NatPayload Z) Nat which is identical to Nat after beta reduction.

Observed Behavior

A type error prevent compilation of a correct program.

When checking right hand side of zero with expected type
        Nat

Type mismatch between
        (NatPayload Z) *-> Nat (Type of MkNat Z)
and
        Nat (Expected type)

Specifically:
        Type mismatch between
                function (NatPayload Z) Nat
        and
                Nat

[ahmadsalim]

@JadenGeller Thanks for reporting the issue.
This is expected behaviour, since Idris will not reduce any function in types which are in the same mutual block. A better error message could be provided though.

[JadenGeller]

Is it expected that the error does not resolve when I move functions that needn't be in mutual out of mutual?

data NatTag = Z | S

mutual
    NatPayload : NatTag -> List Type
    NatPayload Z = []
    NatPayload S = [Nat]

    Nat : Type
    Nat = AlgebraicData NatTag NatPayload
   
MkNat : (tag : NatTag) -> NatPayload tag *-> Nat
MkNat = MkAlgebraicData

elimNat : ((tag : NatTag) -> NatPayload tag *-> a) -> Nat -> a
elimNat = elimAlgebraicData

There's now a type error even earlier, in MkNat!

When checking right hand side of MkNat with expected type
        (tag : NatTag) -> (NatPayload tag) *-> Nat

Type mismatch between
        (tag : NatTag) ->
        (Payload tag) *-> AlgebraicData NatTag Payload (Type of MkAlgebraicData)
and
        (tag : NatTag) -> function (NatPayload tag) Nat (Expected type)

Specifically:
        Type mismatch between
                function (Payload v0) (AlgebraicData NatTag Payload)
        and
                function (NatPayload v0) Nat
Holes: Main.MkNat

[ahmadsalim]

@JadenGeller Yes, because NatPayload does not reduce to a list, because the tag variable value is unknown.

[JadenGeller]

Even when the tag is known, it doesn't seem to simply.

data NatTag = Z | S

mutual
    NatPayload : NatTag -> List Type
    NatPayload Z = []
    NatPayload S = [Nat]

    Nat : Type
    Nat = AlgebraicData NatTag NatPayload
   
zero : Nat
zero = MkAlgebraicData Z {Payload=NatPayload}

In the following error, the tag is known to be Z, but NatPayload Z does not simplify:

When checking right hand side of zero with expected type
        Nat

Type mismatch between
        (NatPayload Z) *-> AlgebraicData NatTag NatPayload (Type of MkAlgebraicData Z)
and
        Nat (Expected type)

Specifically:
        Type mismatch between
                function (NatPayload Z) (AlgebraicData NatTag NatPayload)
        and
                Nat

If I try to simplify function (NatPayload Z) (AlgebraicData NatTag NatPayload) in the REPL, it does work, evaluating to AlgebraicData NatTag NatPayload (aka Nat). This seems to imply something is broken.

[JadenGeller]

I also wouldn't expect {Payload=NatPayload} to be necessary, but that's a separate bug, I think.

[ahmadsalim]

@JadenGeller There are limits of what Idris can do automatically, because higher-order unification is incomplete (so e.g., it would not try unify the non-injective NatPayload with Payload).

Also, it does not know what Payload Z reduces to since it is not a function. You may need to use some explicit proofs or pass parameters explicitly to get this working.

[ahmadsalim]

@JadenGeller I think that the issue is that in your case, you are passing NatPayload as a parameter after the explicit parameter which is wrong. It should work if you switch the order (I don't know why it does not complain here).

[JadenGeller]

@ahmadsalim I had pasted the wrong error. Explicitly passing the implicit parameter first fails in the same exact way it does when I pass it second.

When checking right hand side of zero with expected type
        Nat

Type mismatch between
        (NatPayload Z) *-> AlgebraicData NatTag NatPayload (Type of MkAlgebraicData Z)
and
        Nat (Expected type)

Specifically:
        Type mismatch between
                function (NatPayload Z) (AlgebraicData NatTag NatPayload)
        and
                Nat

These expressions are clearly beta equivalent, no?

[ahmadsalim]

@JadenGeller Try using %default total on top of your file and see if it complains somewhere.

[JadenGeller]

It looks like it is unable to verify totality for Nat and NatPayload. Any trick to prove it?

[ahmadsalim]

@JadenGeller You need a way to show that the recursion decreases in size, how would you ensure this in this case? As far as I can see now, it does not need to.

An alternative is to use some type of fuel, that you decrease on each recursion.

[JadenGeller]

It seems silly to have to prove that though, no? It doesn't decrease in size in the same way that

data Nat : Type where
    Z : Nat
    S : Nat -> Nat

doesn't decrease in size when you apply S over and over and over again forever. But you couldn't construct that value without breaking totality elsewhere!

Just like construction of S (S (S (S (S …)))) is guarded by the S constructor, construction of MkNat S (MkNat S (MkNat S …)) is guarded by the MkAlgebraicDataRaw constructor.

[JadenGeller]

I feel like this is related to productivity checking v. decreasing argument checking, right? I know Agda has a way to mark records as coinductive. Would this be useful here?

[JadenGeller]

All recursive calls do seem to be constructor guarded, so I would expect this to be verified as total by means of productivity.

[david-christiansen]

If you want to use productivity instead of termination, then the productive bit needs to be wrapped in Inf.

[ahmadsalim]

@JadenGeller You are here running into a meta-theoretical problem which Idris can not solve easily.
For data-types Idris has simple ways to solve the induced recursive algebraic equations, where it uses a positivity checker to check that these (iso-recursive) equations form a correct initial algebra.

However, when you introduce these recursive type equations explicitly, the theory of Idris has currently no way of determining whether these sets of recursive equations form a valid type. In fact, solving recursive type equations nicely has been a research topic for decades, and you need to use one of these approaches if you want to have your solution be accepted in Idris.
To do this you may want to take a look at something like The Gentle Art of Levitation or the background section in my MSc thesis The Practical Guide to Levitation.
Alternative approaches include using Domain Theory, Guarded Recursion, Step-indexed logical relations or similar to calculate least/greatest fixpoint solutions for these recursive equations.

[ahmadsalim]

See also some of the files (like internalMu) here https://github.com/gallais/potpourri/tree/master/agda/poc