Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#12668 closed bug (fixed)

Program that fails Core Lint terribly

Reported by: bgamari Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler (Type checker) Version: 8.1
Keywords: LevityPolymorphism Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T12668
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

While looking for a testcase for another unrelated compiler bug (see Phab:D2577) I had the pleasure of encountering this specimen,

{-# LANGUAGE TypeInType #-}
{-# LANGUAGE RankNTypes #-}
module Hi where

import GHC.Exts

data Some r = Some (TYPE r -> TYPE r)

doSomething :: forall (r :: RuntimeRep). forall (a :: TYPE r). ()
            => Int -> (a -> Int) -> a -> a
doSomething n f =
    case n of
      1 -> error "hello"
      3 -> error "hello"

GHC 465c6c5d15f8fb54afb78408f3a79e75e74d2cd4 and 8.0.1 seem to let this program typecheck, but if you enable Core Lint it soon becomes clear that not all is well. Here's a sampling of the carnage,

$ ghc hi.hs -fforce-recomp -dcore-lint -O0
[1 of 1] Compiling Hi               ( hi.hs, hi.o )
*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: warning:
    In the type ‘a_a2ON -> Int’
    Ill-kinded argument in type or kind ‘a_a2ON -> Int’
    type or kind ‘a_a2ON -> Int’ kind: TYPE r_a2OM
<no location info>: warning:
    In the type ‘a_a2ON -> a_a2ON’
    Ill-kinded argument in type or kind ‘a_a2ON -> a_a2ON’
    type or kind ‘a_a2ON -> a_a2ON’ kind: TYPE r_a2OM
<no location info>: warning:
    In the type ‘a_a2ON -> a_a2ON’
    Ill-kinded argument in type or kind ‘a_a2ON -> a_a2ON’
    type or kind ‘a_a2ON -> a_a2ON’ kind: TYPE r_a2OM
<no location info>: warning:
    In the expression: patError
                         @ 'PtrRepLifted @ (a_a2ON -> a_a2ON) "hi.hs:(12,5)-(14,24)|case"#
    Ill-kinded argument in type or kind ‘a_a2ON -> a_a2ON’
    type or kind ‘a_a2ON -> a_a2ON’ kind: TYPE r_a2OM
...

Change History (6)

comment:1 Changed 3 years ago by bgamari

Description: modified (diff)

comment:2 Changed 3 years ago by goldfire

What's wrong here? My first worry is that Core Lint is doing the wrong thing. And does your Some type enter the picture?

comment:3 Changed 3 years ago by bgamari

What's wrong here? My first worry is that Core Lint is doing the wrong thing.

I'm afraid I didn't look much farther; I was hoping I'd be able to quickly get the typeable branch rebased between builds on another project; sadly the yaks just keep piling up.

And does your Some type enter the picture?

Indeed I suspect it doesn't.

comment:4 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In eefe86d/ghc:

Allow levity-polymorpic arrows

This cures Trac #12668 (and cures the Lint errors you get from
Trac #12718).

The idea is explained in Note [Levity polymorphism], in Kind.hs

comment:5 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: polykinds/T12668

comment:6 Changed 3 years ago by bgamari

Keywords: LevityPolymorphism added
Note: See TracTickets for help on using tickets.