[GHC] #16225: GHC HEAD-only Core Lint error (Trans coercion mis-match)

[GHC]

#16225: GHC HEAD-only Core Lint error (Trans coercion mis-match)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.7
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #16188, #16204
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following code compiles on GHC 8.0.2 through GHC 8.6.3 with `-dcore-
 lint`:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind

 data family Sing :: k -> Type
 data TyFun :: Type -> Type -> Type
 type a ~> b = TyFun a b -> Type
 infixr 0 ~>
 type family Apply (f :: a ~> b) (x :: a) :: b

 data TyCon1 :: (k1 -> k2) -> (k1 ~> k2)
 type instance Apply (TyCon1 f) x = f x

 data SomeApply :: (k ~> Type) -> Type where
   SomeApply :: Apply f a -> SomeApply f

 f :: SomeApply (TyCon1 Sing :: k ~> Type)
   -> SomeApply (TyCon1 Sing :: k ~> Type)
 f (SomeApply s)
  = SomeApply s
 }}}

 However, it chokes on GHC HEAD:

 {{{
 $ ~/Software/ghc4/inplace/bin/ghc-stage2 --interactive Bug.hs -dcore-lint
 GHCi, version 8.7.20190120: https://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 *** Core Lint errors : in result of Desugar (before optimization) ***
 <no location info>: warning:
     In the expression: SomeApply
                          @ k_a1Dz
                          @ (TyCon1 Sing)
                          @ Any
                          (s_a1Bq
                           `cast` (Sub (D:R:ApplyabTyCon1x[0]
                                            <k_a1Dz>_N
                                            <*>_N
                                            <Sing>_N
                                            <a_a1DB>_N ; Sym
 (D:R:ApplyabTyCon1x[0]
 <k_a1Dz>_N <*>_N <Sing>_N <Any>_N))
                                   :: Apply (TyCon1 Sing) a_a1DB ~R# Apply
 (TyCon1 Sing) Any))
     Trans coercion mis-match: D:R:ApplyabTyCon1x[0]
                                   <k_a1Dz>_N <*>_N <Sing>_N <a_a1DB>_N ;
 Sym (D:R:ApplyabTyCon1x[0]
 <k_a1Dz>_N
 <*>_N
 <Sing>_N
 <Any>_N)
       Apply (TyCon1 Sing) a_a1DB
       Sing a_a1DB
       Sing Any
       Apply (TyCon1 Sing) Any
 *** Offending Program ***

 <elided>

 f :: forall k. SomeApply (TyCon1 Sing) -> SomeApply (TyCon1 Sing)
 [LclIdX]
 f = \ (@ k_a1Dz) (ds_d1EV :: SomeApply (TyCon1 Sing)) ->
       case ds_d1EV of wild_00 { SomeApply @ a_a1DB s_a1Bq ->
       break<0>(s_a1Bq)
       SomeApply
         @ k_a1Dz
         @ (TyCon1 Sing)
         @ Any
         (s_a1Bq
          `cast` (Sub (D:R:ApplyabTyCon1x[0]
                           <k_a1Dz>_N <*>_N <Sing>_N <a_a1DB>_N ; Sym
 (D:R:ApplyabTyCon1x[0]
 <k_a1Dz>_N
 <*>_N
 <Sing>_N
 <Any>_N))
                  :: Apply (TyCon1 Sing) a_a1DB ~R# Apply (TyCon1 Sing)
 Any))
       }
 }}}

 Note that if I change the definition of `Sing` to this:

 {{{#!hs
 data family Sing (a :: k)
 }}}

 Then the error goes away.

 Also, if I extend `SomeProxy` with an additional `proxy` field:

 {{{#!hs
 data SomeApply :: (k ~> Type) -> Type where
   SomeApply :: proxy a -> Apply f a -> SomeApply f

 f :: SomeApply (TyCon1 Sing :: k ~> Type)
   -> SomeApply (TyCon1 Sing :: k ~> Type)
 f (SomeApply p s)
  = SomeApply p s
 }}}

 Then the error also goes away. Perhaps `a` being ambiguous plays an
 important role here?

 Possibly related to #16188 or #16204.

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