#14038: TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: () -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.3 checker) | Keywords: Resolution: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): My local fix for #12919 ''does'' fix this. But then a deeper bug lurks. The problem is that the `App` instance for `(:~>)` gets type-checked with a coercion in its patterns. Of course, the type-family matcher can't deal with a coercion pattern -- what would such a thing mean anyway? So it does something stupid. In this case, the stupid thing is that the match result contains an unbound variable, but it could conceivably do a different stupid thing tomorrow. The solution, of course, is to make sure that type patterns never contain coercions. I've been meaning to do this for a long time, regardless. (I don't think there's a ticket to track the idea, though.) I see two possible approaches: 1. Parameterize the code in TcHsType to know whether it's reading a pattern or a normal type, and don't make coercions in patterns. 2. Have TcHsType proceed normally, but rip the coercions out after-the- fact. What to do in the spots where the coercions used to be? Insert bare coercion variables, which can then be solved for. Some perhaps-outdated thoughts on this are [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Matchingaxio... here], but those notes were meant more for myself than anyone else. While we're thinking about this, another question I've pondered for a while: should type patterns be a separate datatype in GHC than `Type`? For example, a type pattern never has a type function nor a forall. It won't have meaningful `CastTy`s or `CoercionTy`s either. With this change, the pure unifier could perhaps be simplified. In any case, more thought is necessary. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14038#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler