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

6 Mar 2019

      #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