Lint error in forall type

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

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

8------->8------->8--- ..\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->

changed weight to 5

added StaticPointers Tbug Trac import labels

Smaller version:

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

changed title from StaticPointers + -dcore-lint: cause Core Lint error?? to 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.

mentioned in commit 9d600ea6

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

I've commented on the commit on Phab. You're right that typeKind is wrong in this same way.

mentioned in issue #15276 (closed)

added Pnormal label

typeKind was fixed in f903e551 and later polished in #16391 (closed).

I believe everything is done - closing.

closed