Opened 2 years ago
Last modified 23 months ago
#11424 new bug
"Occurs check" not considered when reducing closed type families
Reported by: | diatchki | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.1 |
Keywords: | TypeFamilies | Cc: | |
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
Hello,
consider the following example:
{-# 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)
Change History (8)
comment:1 Changed 2 years ago by
comment:2 follow-up: 3 Changed 2 years ago by
Perhaps there is a different way to do the reduction that avoids this problem. My mental model of type functions is that:
- they only ever *name* types, they never introduce *new* types, which arise from
data
,newtype
and primitives. - 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.
comment:3 Changed 2 years ago by
Replying to 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 my blog post on the subject (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.
comment:4 follow-up: 5 Changed 2 years ago by
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.
comment:5 Changed 2 years ago by
Replying to diatchki:
If by
x
you mean a type variable, then I don't think there is any problem in reducingEquals x x
toTrue
.Otoh, if you encountered
Equals (F a) (F a)
, then you can still reduce that toTrue
, but you'd also have to emit the constraintF a ~ b
, to make sure thatF 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.
comment:6 Changed 23 months ago by
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").
comment:7 Changed 23 months ago by
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.
comment:8 Changed 23 months ago by
Keywords: | TypeFamilies added |
---|
What if 'a' was instantiated with
Loopy Int
whereNow indeed if we see
Same (Loopy Int) [Loopy Int]
we could reduce it toInt
.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