[GHC] #11511: Type family producing infinite type accepted as injective
#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 (Type checker) | Keywords: TypeFamilies, | Operating System: Unknown/Multiple Injective | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- A question came up during discussion at University of Wrocław: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: TypeFamilies, Resolution: | Injective Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) Comment: 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.] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: TypeFamilies, Resolution: | Injective Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: TypeFamilies, Resolution: | Injective Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: TypeFamilies, Resolution: | Injective Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: TypeFamilies, Resolution: | Injective Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: TypeFamilies, Resolution: | Injective Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: TypeFamilies, Resolution: | Injective Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11511: Type family producing infinite type accepted as injective -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeFamilies, Injective => TypeFamilies, InjectiveFamilies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11511#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC