#15952: Reduce zonking-related invariants in the type checker -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 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): A call this week clarified a few things: A. The second commit in comment:3 exposed an underlying bug. That is, we sometimes call `typeKind` in the type checker. This calls `piResultTys`. But `piResultTys` calls `substTy`, when really we need `nakedSubstTy`. We ''could'' make `tc` equivalents for all these to fix the problem. But better is just to go ahead with the plan in this ticket, which also fixes the problem. B. I've expressed worry about `substTy` encountering a `TcTyVar`. But we realized what's really going on: every substitution (in the type-checker) morally has a `TcLevel`. Substituting variables ''at or above'' that level is highly bogus. But substituting variables ''below'' that level is fine -- they're effectively rigid anyway. In practice, this means that we can instantiate polytypes that still mention meta-type-variables, ''as long as the levels are below the level of the substitution''. Should we actually track and check this? Probably not. But it's good to understand what's going on. This should be put in a Note. C. It's unclear what the advantages/disadvantages are of removing the second return value from `tc_infer_hs_type`. In the last, fallthrough case of that function, it might be quite a lot easier to return the kind rather than reconstruct it. I conjecture that this is purely a performance issue, not at all a correctness issue. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15952#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler