Re: [GHC] #14038: TypeApplications regression in GHC HEAD: ‘p0’ is untouchable inside the constraints: ()

[GHC]

#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#Matchingaxioms
 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