#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] _N <*>_N <Sing>_N _N ; Sym (D:R:ApplyabTyCon1x[0] _N <*>_N <Sing>_N <Any>_N)) :: Apply (TyCon1 Sing) a_a1DB ~R# Apply (TyCon1 Sing) Any)) Trans coercion mis-match: D:R:ApplyabTyCon1x[0] _N <*>_N <Sing>_N _N ; Sym (D:R:ApplyabTyCon1x[0] _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] _N <*>_N <Sing>_N _N ; Sym (D:R:ApplyabTyCon1x[0] _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