#15664: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Short version {{{#!hs {-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-} {-# Options_GHC -dcore-lint #-} import Data.Kind type family Apply (kind) (f :: kind) :: Type data ApplyT(kind) :: kind -> Type type f ~> g = (forall xx. f xx -> g xx) unravel :: ApplyT(k) ~> Apply(k) unravel = unravel }}} {{{ $ ghci -ignore-dot-ghci hs/443.hs GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( hs/443.hs, interpreted ) *** Core Lint errors : in result of Desugar (before optimization) *** <no location info>: warning: In the type ‘forall k. ApplyT k ~> Apply k’ Un-saturated type application Apply k_a1y2 *** Offending Program *** Rec { $tcApplyT :: TyCon [LclIdX] $tcApplyT = TyCon 14646326419187070856## 770477529860249545## $trModule (TrNameS "ApplyT"#) 1# $krep_a1Ad $krep_a1Ae [InlPrag=NOUSERINLINE[~]] :: KindRep [LclId] $krep_a1Ae = $WKindRepVar (I# 0#) $krep_a1Ad [InlPrag=NOUSERINLINE[~]] :: KindRep [LclId] $krep_a1Ad = KindRepFun $krep_a1Ae krep$* $trModule :: Module [LclIdX] $trModule = Module (TrNameS "main"#) (TrNameS "Main"#) unravel :: forall k. ApplyT k ~> Apply k [LclIdX] unravel = \ (@ k_a1zb) (@ (xx_a1zc :: k_a1zb)) -> break<0>() unravel @ k_a1zb @ xx_a1zc end Rec } *** End of Offense *** <no location info>: error: Compilation had errors *** Exception: ExitFailure 1

}}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15664#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15664: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"4bdb10ca7ba14f00dd62270eadab4f93238227bc/ghc" 4bdb10ca/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="4bdb10ca7ba14f00dd62270eadab4f93238227bc" Fix Lint of unsaturated type families GHC allows types to have unsaturated type synonyms and type families, provided they /are/ saturated if you expand all type synonyms. TcValidity carefully checked this; see check_syn_tc_app. But Lint only did half the job, adn that led to Trac #15664. This patch just teaches Core Lint to be as clever as TcValidity. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15664#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15664: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T15664 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:

From [https://github.com/VictorCMiraldo/victorcmiraldo.github.io/blob/845e74b59aee... Generic Programming of All Kinds],

{{{#!hs {-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-}

{-# Options_GHC -dcore-lint #-}

-- https://github.com/VictorCMiraldo/victorcmiraldo.github.io/blob/845e74b59aee...

import Data.Kind import GHC.Exts import Data.Function

data Ctx :: Type -> Type where E :: Ctx(Type) (:&:) :: a -> Ctx(as) -> Ctx(a -> as)

type family Apply(kind) (f :: kind) (ctx :: Ctx kind) :: Type where Apply(Type) a E = a Apply(k -> ks) f (a:&:as) = Apply(ks) (f a) as

data ApplyT kind :: kind -> Ctx(kind) -> Type where A0 :: a -> ApplyT(Type) a E

AS :: ApplyT(ks) (f a) as -> ApplyT(k -> ks) f (a:&:as)

type f ~> g = (forall xx. f xx -> g xx)

unravel :: ApplyT(k) f ~> Apply(k) f unravel (A0 a) = a unravel (AS fa) = unravel fa }}}

gives a core lint error

{{{ $ ghci -ignore-dot-ghci hs/443.hs > /tmp/bug.log }}}

New description: From [https://dl.acm.org/citation.cfm?id=3242745 Generic Programming of All Kinds], {{{#!hs {-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-} {-# Options_GHC -dcore-lint #-} import Data.Kind import GHC.Exts import Data.Function data Ctx :: Type -> Type where E :: Ctx(Type) (:&:) :: a -> Ctx(as) -> Ctx(a -> as) type family Apply(kind) (f :: kind) (ctx :: Ctx kind) :: Type where Apply(Type) a E = a Apply(k -> ks) f (a:&:as) = Apply(ks) (f a) as data ApplyT kind :: kind -> Ctx(kind) -> Type where A0 :: a -> ApplyT(Type) a E AS :: ApplyT(ks) (f a) as -> ApplyT(k -> ks) f (a:&:as) type f ~> g = (forall xx. f xx -> g xx) unravel :: ApplyT(k) f ~> Apply(k) f unravel (A0 a) = a unravel (AS fa) = unravel fa }}} gives a core lint error {{{ $ ghci -ignore-dot-ghci hs/443.hs > /tmp/bug.log }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15664#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler