#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932 -------------------------------------+------------------------------------- Reporter: thomie | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeInType 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):
I'm not sure what you mean by "quite different"
Suppose you instantiate `f :: forall k. forall (a :: kappa). blah` at some call site. Make up a fresh meta-var for `k` and substitute. We won't substitute for `kappa` because it isn't `k`. Later we unify `kappa := k`. And now our earlier instantiation of `f`'s type is utterly wrong. Actually the real INVARIANT is probably this: * In any quantified type `forall a. blah`, all occurrences of `a` in `blah` must be manifest: not hidden inside meta-tyvars, especially if they have not been instantiated. There could in principle be some free meta-tyvars that we somehow know can never be filled in with the quantified type variable. But for top-level types or kinds this is never necessary. Anyway I agree with your plan. But
But I don't spot a missing `solveEqualities` anywhere. Did you miss the call toward the top of `kcTyClGroup`?
I'm still looking at `kcHsTyVarBndrs`. It builds a polytype with `mkSpecForAllTys`. It does unification (inside the call to `tcHsTyVarBndr_Scoped`). I think we need to solve the equalities before we bind the type variables that are mentioned, don't we? Ugh -- that `kcHsTyVarBndrs` is horribly complicated. We should probably Skype but I'm out all Thurs. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11648#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler