[GHC] #11424: "Occurs check" not considered when reducing closed type families
#11424: "Occurs check" not considered when reducing closed type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Hello, consider the following example: {{{#!hs {-# LANGUAGE TypeFamilies #-} type family Same a b where Same a a = Int Same a b = Char example :: Same a [a] -> a example = undefined bad :: a bad = example 'c' }}} This program should type check, using the following reasoning: `a` and `[a]` can never be equal, therefore the first equation for `Same` does not apply, and so we can fall trough to the second one, thus reducing `Same` to `Char`. Therefore, `bad` should be accept. GHC rejects this program with the following error: {{{ • Couldn't match expected type ‘Same a [a]’ with actual type ‘Char’ • In the first argument of ‘example’, namely ‘'c'’ In the expression: example 'c' In an equation for ‘bad’: bad = example 'c' • Relevant bindings include bad :: a (bound at tmp/test.hs:11:1) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11424: "Occurs check" not considered when reducing closed type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: 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 simonpj): What if 'a' was instantiated with `Loopy Int` where {{{ type family Loop x type instance Loopy Int = [Loopy Int] }}} Now indeed if we see `Same (Loopy Int) [Loopy Int]` we could reduce it to `Int`. This is all very tiresome I know. It's discussed at some length in our "Closed type families" paper. If you can think of a better solution than what we propose there, we're all ears. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11424: "Occurs check" not considered when reducing closed type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: 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 diatchki): Perhaps there is a different way to do the reduction that avoids this problem. My mental model of type functions is that: 1. they only ever ***name*** types, they never introduce ***new*** types, which arise from `data`, `newtype` and primitives. 2. they may be partial, so sometimes they don't name any type at all. I find it easiest to think about all this in terms of GHC's internal representation of the constraints, so your example would look something like this: {{{ (Same a [a] ~ Char, Loop Int ~ a) }}} Now, I think reducing `Same a [a] ~ Char` to `Char ~ Char`, and then just eliminating it as a trivial equality is perfectly valid. However, eliminating the `Loop Int ~ a` constraint is what's questionable here, even if `a` is not used anywhere. This constraint essentially says that `Loop Int` must be well-defined, in other words, it better refer to an actual ground type that exists. One (fairly simple?) way for GHC to check the validity of such constraints would be to simply evaluate them until it does find the ground type in question. In your example, this would result in GHC non-terminating during type checking, which is perfectly reasonable, especially since you need `UndecidableInstaces` to write such recursive types. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11424: "Occurs check" not considered when reducing closed type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: 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): Replying to [comment:2 diatchki]:
One (fairly simple?) way for GHC to check the validity of such constraints would be to simply evaluate them until it does find the ground type in question. In your example, this would result in GHC non- terminating during type checking, which is perfectly reasonable, especially since you need `UndecidableInstaces` to write such recursive types.
Except that means that type families can't work over abstract types that we don't know much about yet. For example: {{{ type family Equals a b where Equals a a = True Equals a b = False }}} I `Equals x x` to reduce to `True` even if I don't know what `x` is. Under your scheme, I would need to know what `x` is to be able to make progress, if only to ensure that it terminates. This whole thing is a sad story. But I don't know how to make it better. See also #10327 and [https://typesandkinds.wordpress.com/2015/09/09/what- are-type-families/ my blog post] on the subject ([https://www.reddit.com/r/haskell/comments/3kyfrl/richard_eisenberg_what_are_... reddit comments on blog post]). Bottom line: I think the Right Solution is to require all non-associated type families to be total (implying terminating) and force all non-total type families to be associated with a class constraint. (This actually makes them functional dependencies in disguise!) Then these problems go away. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11424: "Occurs check" not considered when reducing closed type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: 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 diatchki): I am not sure what you mean by "abstract types". If by `x` you mean a type variable, then I don't think there is any problem in reducing `Equals x x` to `True`. Otoh, if you encountered `Equals (F a) (F a)`, then you can still reduce that to `True`, but you'd also have to emit the constraint `F a ~ b`, to make sure that `F a` is well-defined. I do agree that if we can't prove that a type family is total, it essentially should have a well-formedness check on every use---in this example this is `F a ~ b`, but one may have some other class/constraint encoding the same thing too. One may also think of this the other way: we always emit a well-formedness constraint on use, but if we've proved that a type function is total, then we can solve this constraint trivially. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
If by `x` you mean a type variable, then I don't think there is any
#11424: "Occurs check" not considered when reducing closed type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: 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): Replying to [comment:4 diatchki]: problem in reducing `Equals x x` to `True`.
Otoh, if you encountered `Equals (F a) (F a)`, then you can still reduce
that to `True`, but you'd also have to emit the constraint `F a ~ b`, to make sure that `F a` is well-defined.
But this doesn't support the substitution lemma. You say that we can reduce `Equals x x`. But what if we later learn that `x` is really `F a`? So if we're going to do the well-definedness check in the `F a` case, we have to delay reducing the `x` case. I agree with the other points in comment:4. Instead of a general well- formedness check, I'm asking the users to provide the name of a class that represents well-formedness. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11424: "Occurs check" not considered when reducing closed type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: 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 diatchki): I don't think that a direct "substitution" lemma makes sense in this context---remember that `F a` may not refer to a type at all, so we can't just put it in a place where a type is expected. So, if we had some type-expression `t`, and wanted to substitute `F a` for some variable `b`, we wouldn't do a direct substitution, but rather, we'd emit a new constraint: `F a ~ b`. Basically, the idea is that type functions are not really first class types, but may "introduce" types via constraints like: `F a ~ b`. So, if I write a type like `Maybe (F a)`, what I really mean is `(F a ~ b) => Maybe b`. Of course, if we can prove that `F a` is always defined we may "short-cut" the constraint part and just treat it as an ordinary type, but that's optional. This is basically the same idea is the "functional notation for functional dependencies" (section 3 of "Language and Program Design for Functional Dependencies"). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11424: "Occurs check" not considered when reducing closed type families -------------------------------------+------------------------------------- Reporter: diatchki | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: 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): Yes. I think we're vigorously agreeing. Except that this is quite far from the way GHC works at the moment, and it's not a small change to make. I do think it's the right answer, in the end. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11424#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC