[GHC] #14939: StaticPointers + -dcore-lint: cause Core Lint error??
#14939: StaticPointers + -dcore-lint: cause Core Lint error?? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple StaticPointers | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This is an odd bug {{{#!hs {-# Language StaticPointers #-} import Data.Kind type Cat ob = ob -> ob -> Type type Alg cls ob = ob newtype Frí (cls::Type -> Constraint) :: (Type -> Alg cls Type) where Frí :: { with :: forall x. cls x => (a -> x) -> x } -> Frí cls a data AlgCat (cls::Type -> Constraint) :: Cat (Alg cls Type) where AlgCat :: (cls a, cls b) => (a -> b) -> AlgCat cls a b leftAdj :: AlgCat cls (Frí cls a) b -> (a -> b) leftAdj (AlgCat f) a = undefined }}} causes a {{{ $ ./ghc-stage2 --interactive -ignore-dot-ghci -dcore-lint 222-bug.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 222-bug.hs, interpreted ) *** Core Lint errors : in result of Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = False}) *** <no location info>: warning: In the type ‘forall (cls :: * -> Constraint) (b :: Alg cls *). b’ Variable escape in forall: forall (cls :: * -> Constraint) (b :: Alg cls *). b *** Offending Program *** with :: forall (cls :: * -> Constraint) a. Frí cls a -> forall x. cls x => (a -> x) -> x [LclIdX[[RecSel]], Arity=2] with .. . --->8------->8------->8--- .. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14939 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14939: StaticPointers + -dcore-lint: cause Core Lint error?? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | StaticPointers 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 monoidal): Smaller version: {{{#!haskell {-# Language StaticPointers, TypeInType, GADTs #-} import Data.Kind type Alg cls = Type data AlgCat (cls::Type) :: Alg cls -> Type where leftAdj :: AlgCat cls a -> a leftAdj f = undefined }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14939#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14939: Lint error in forall type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | StaticPointers 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 simonpj): The Lint error is this: {{{ In the type `forall (cls :: * -> Constraint) (b :: Alg cls *). b' Variable escape in forall: forall (cls :: * -> Constraint) (b :: Alg cls *). b }}} The complaint is because the kind of the body of the forall is `Alg cls *`, but the forall binds `cls` so it looks as if `cls` escapes. But actually it is fine because {{{ type Alg cls ob = ob }}} so `Alg cls *` is really just `*`, and the `cls` argument is not mentioned in the expansion. I conclude that the program is fine and it's Lint that is at fault. c.f. `TcUnify.occCheckExpand` and `CoreUtils.coreAltsType` which deal with the same problem. A single systematic solution eludes me. I worry that `Type.typeKind` suffers from the same problem, in the `ForAllTy` case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14939#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14939: Lint error in forall type
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.5
Resolution: | Keywords:
| StaticPointers
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
#14939: Lint error in forall type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | StaticPointers 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 simonpj): Richard, I'd be interested in what you think here, esp re `typeKind`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14939#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14939: Lint error in forall type -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | StaticPointers 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 goldfire): I've commented on the commit on Phab. You're right that `typeKind` is wrong in this same way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14939#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC