Opened 8 months ago

Last modified 6 months ago

## #14939 new bug

# Lint error in forall type

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 8.5 |

Keywords: | StaticPointers | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

This is an odd bug

{-# 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--- ..

### Change History (5)

### comment:1 Changed 8 months ago by

### comment:2 Changed 6 months ago by

Summary: | StaticPointers + -dcore-lint: cause Core Lint error?? → Lint error in forall type |
---|

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.

### comment:4 Changed 6 months ago by

Richard, I'd be interested in what you think here, esp re `typeKind`

.

### comment:5 Changed 6 months ago by

I've commented on the commit on Phab. You're right that `typeKind`

is wrong in this same way.

**Note:**See TracTickets for help on using tickets.

Smaller version: