[GHC] #15918: mkCastTy sometimes drops insoluble (Type ~ Constraint) coercions (was: GHC panic from QuantifiedConstraints(?))

[GHC]

#15918: mkCastTy sometimes drops insoluble (Type ~ Constraint) coercions
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               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:  quantified-
                                     |  constraints/T15918
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/489
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * keywords:  QuantifiedConstraints =>
 * milestone:  8.10.1 => ⊥


Old description:

> Minimized from
> https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I
> don't expect `Build []` to kind check but ti shouldn't crash.
>
> {{{#!hs
> {-# Language PolyKinds             #-}
> {-# Language TypeFamilies          #-}
> {-# Language ConstraintKinds       #-}
> {-# Language FlexibleContexts      #-}
> {-# Language QuantifiedConstraints #-}
> {-# Language UndecidableInstances  #-}
>
> import Data.Kind
>
> class Rev f where
>   rev :: f a
>
> instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where
>   rev = undefined
>
> data Build :: ((k -> Type) -> Constraint) -> (k -> Type)
>
> uu = rev :: Build [] a
> }}}
>
> gives a panic
>
> {{{
> $ ./ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs
> GHCi, version 8.7.20181029: http://www.haskell.org/ghc/  :? for help
> [1 of 1] Compiling Main             ( ~/hs/711_bug.hs, interpreted )
> ghc-stage2: panic! (the 'impossible' happened)
>   (GHC version 8.7.20181029 for x86_64-unknown-linux):
>         ASSERT failed!
>   irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})]
>   Call stack:
>       CallStack (from HasCallStack):
>         callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in
> ghc:Outputable
>         pprPanic, called at compiler/utils/Outputable.hs:1219:5 in
> ghc:Outputable
>         assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in
> ghc:TcType
>
> Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
>
> >
> }}}

New description:

 EDIT: See comment:3 for the real cause and comment:17 for the current
 plan.
 ---------------------------

 Minimized from
 https://gist.github.com/Icelandjack/683bd4b79027695ffc31632645c9d58b, I
 don't expect `Build []` to kind check but ti shouldn't crash.

 {{{#!hs
 {-# Language PolyKinds             #-}
 {-# Language TypeFamilies          #-}
 {-# Language ConstraintKinds       #-}
 {-# Language FlexibleContexts      #-}
 {-# Language QuantifiedConstraints #-}
 {-# Language UndecidableInstances  #-}

 import Data.Kind

 class Rev f where
   rev :: f a

 instance (forall xx. cls xx => Rev xx) => Rev (Build cls) where
   rev = undefined

 data Build :: ((k -> Type) -> Constraint) -> (k -> Type)

 uu = rev :: Build [] a
 }}}

 gives a panic

 {{{
 $ ./ghc-stage2 --interactive -ignore-dot-ghci ~/hs/711_bug.hs
 GHCi, version 8.7.20181029: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( ~/hs/711_bug.hs, interpreted )
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 8.7.20181029 for x86_64-unknown-linux):
         ASSERT failed!
   irred_a1zW :: [(xx_a1zV[sk:3] |> Sym {co_a1zu})]
   Call stack:
       CallStack (from HasCallStack):
         callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in
 ghc:Outputable
         pprPanic, called at compiler/utils/Outputable.hs:1219:5 in
 ghc:Outputable
         assertPprPanic, called at compiler/typecheck/TcType.hs:1826:53 in
 ghc:TcType

 Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 >
 }}}

--

Comment:

 I think we decided to punt.

 comment:11 reports that the original bug is fixed. In addition, this
 ticket's friend #15799 is also no longer triggering. So I think the
 underlying bug here is real, but it's both difficult (impossible?) to
 trigger and difficult to fix. Furthermore, the bug can only strike in
 ''incorrect'' programs. This bug ''cannot'' make ill-typed Core. All of
 this suggests that we take my personal favorite course of action: do
 nothing.

 I've retitled the ticket to be more informative and will set the milestone
 accordingly. But I don't quite want to close the ticket, because I do
 believe there is a real bug here. Perhaps someday we'll find a way to
 trigger this ticket, making it more worthwhile to invest in a fix.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15918#comment:17>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler