Scope type vars when type checking typed values #4216
Conversation
When the compiler is checking an expression that is annotated with a type against another expected type, and the annotation introduces a type variable, the compiler needs to introduce that type variable to the scope of any types used inside the expression. One noteworthy case of this pattern is member signatures inside instances. This fix allows type variables introduced in member signatures to be used in the member declaration itself.
rhendric
force-pushed
the
rhendric/fix-2941
branch
from
ea132fc to
662213e
Compare
|
Does this also fix it so you can use a type variable introduced in an instance head, or does it only apply to member annotations? If it fixes the former too it'd be nice to have a test for that! |
|
If you're talking about |
|
Ah, actually looks like the thing I meant already works! I guess I'd just mixed it up in my head with the case you've fixed here. I meant this kind of thing: data I a = I a
class Foo a where
something ∷ Unit → a
instance Monoid a ⇒ Foo (I a) where
something _ = I (mempty ∷ a) |
rhendric
force-pushed
the
rhendric/fix-2941
branch
from
662213e to
3b23adf
Compare
|
I restarted CI, thinking it would include #4217. I guess it doesn't still. |
There was a problem hiding this comment.
Explaining this code to myself, all this PR is doing is running the same tvToExpr <$> check val ty1' code, except that the withScopedTypeVars now wraps it. And all that function does is amend the environment's types to include additional type variables that one passes into that function. Once the computation finishes, it sets the environment's types back to what it previously was. If any of the new type variables shadow current ones, a warning will be emitted.
These type variables come from kindOfWithScopedVars, which is used in multiple places throughout the TypeChecker/Types.hs file. So, we're not doing anything weird by using it here AFAICT. Lastly, the unsafeCheckCurrentModule just gets the current module's name (should this function be renamed to better indicate that in some future PR?). It's unsafe because if there isn't a current module, there's nothing to return. We use it in other places throughout this file, and our usage here is safe AFAICT.
|
Also worth noting: this PR effectively reverts part of a change made in #2643. But that PR did not change the analogous logic in |
When the compiler is checking an expression that is annotated with a
type against another expected type, and the annotation introduces a type
variable, the compiler needs to introduce that type variable to the
scope of any types used inside the expression.
One noteworthy case of this pattern is member signatures inside
instances. This fix allows type variables introduced in member
signatures to be used in the member declaration itself.
Description of the change
Fixes #2941.
Checklist:
Added myself to CONTRIBUTORS.md (if this is my first contribution)Updated or added relevant documentation