Opened 4 years ago

Last modified 3 years ago

#11511 new bug

Type family producing infinite type accepted as injective

Reported by: jstolarek Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.1
Keywords: TypeFamilies, InjectiveFamilies Cc: goldfire, simonpj, adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

A question came up during discussion at University of Wrocław:

type family F a = r | r -> a where
    F a = [F a]

Should this pass the injectivity check? Currently it does but I don't think this is correct. After all F Bool and F Char both reduce to the same infinite type [[[...]]], which by definition of injectivity gives us Char ~ Bool. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.

This is not an implementation problem - this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.

Change History (8)

comment:1 Changed 4 years ago by adamgundry

Cc: adamgundry added

I don't think this is a soundness problem: FC does not have infinite types, only finite approximations thereof, and there is no way to prove the equality of any finite expansions of F Bool and F Char.

Here's a hand-wavy argument that injectivity of F is admissible... Suppose we have a minimal coercion F s ~ F t. Then either this is by congruence of type family application (in which case we have s ~ t), or it uses the axiom for F to expand both sides, so there is a smaller coercion [F s] ~ [F t] and hence of F s ~ F t (which contradicts the assumption that our original coercion was minimal). [The ordering on coercions is left as an exercise to the reader.]

comment:2 Changed 4 years ago by goldfire

Perhaps this counterexample is why I could never finish that proof. I don't believe I ever reached for an assumption of finite types, probably conflating the notion of finite types with terminating type families.

What bothers me is that we have no guarantee that FC types are indeed finite. On paper, we just define types inductively and are done with it. But how does this play out in the implementation? Recall that infinite types have led to segfaults before: #8162.

comment:3 Changed 4 years ago by jstolarek

I think the right solution here would be to drop equation (7) from our algorithm in the paper.

On a second thought I don't think this would be good idea. Doing this would mean that using any type family in the RHS is prohibited for injective type families and we definitely don't want that for generalized injectivity.

comment:4 Changed 4 years ago by adamgundry

What bothers me is that we have no guarantee that FC types are indeed finite. On paper, we just define types inductively and are done with it. But how does this play out in the implementation?

I suppose it might be possible to accidentally define an "infinite" type or coercion as a lazy value, but surely Core Lint would go into a loop when checking it? What other problems do you envisage?

Recall that infinite types have led to segfaults before: #8162.

That's a slightly different issue: the type family overlap check was unsound because it treated a and a -> a as apart, even though a ~ a -> a is solvable in the presence of non-terminating type families. Crucially, it is possible to construct a finite proof of a ~ a -> a that contradicts the overlap check. Whereas in this case, the only "proofs" of F Bool ~ F Char are infinite (and hence non-constructible).

comment:5 Changed 3 years ago by jstolarek

I had a talk about injective type families yesterday and it provoked me to rethink this issue. What we do in the pre-unification algorithm is:

  1. assume that type family applications unify with anything
  2. but we look under injective type family applications and unify the arguments

Now, my question is: when we are checking whether F is injective why do we assume that F's injectivity annotation is true? This is what we're trying to prove and I think we should not assume that as part of our proof. This is exactly what's happening here.

comment:6 Changed 3 years ago by rwbarton

I imagine you have some examples where you need the recursive assumption. For a boring example, imagine converting one (promoted) unary natural number type data N1 = Z1 | S1 N1 to another data N2 = Z2 | S2 N2:

type family F (a :: N1) :: N2 where
  F Z1 = Z2
  F (S1 n) = S2 (F n)

That is injective but you need to use the injectivity inductively to prove it.

The original example seems fine to me, since you can't prove F Bool ~ F Char (you would need both the "infinite type" [[[...]]] and an infinitely long proof in order to do so).

comment:7 Changed 3 years ago by jstolarek

Yes, certainly what I said is conservative - some injective functions would be rejected. What I'm wondering is whether our current approach is sound from a logical point of view. Perhaps assuming F injective when checking injectivity of F is the reason why Richard couldn't complete the proof we presented in the paper?

comment:8 Changed 3 years ago by simonpj

Keywords: InjectiveFamilies added; Injective removed
Note: See TracTickets for help on using tickets.