Opened 3 weeks ago

Closed 3 weeks ago

Last modified 3 weeks ago

#15664 closed bug (fixed)

Core Lint error

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.6.1-beta1
Keywords: TypeInType Cc:
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 (last modified by Iceland_jack)

From Generic Programming of All Kinds,

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

Attachments (1)

bug.log (15.7 KB) - added by Iceland_jack 3 weeks ago.

Download all attachments as: .zip

Change History (7)

Changed 3 weeks ago by Iceland_jack

Attachment: bug.log added

comment:1 Changed 3 weeks ago by Iceland_jack

Short version

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

comment:2 Changed 3 weeks ago by monoidal

A bit shorter version:

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

{-# Options_GHC -dcore-lint #-}

import Data.Kind

type family Apply (f :: Type) :: Type

type F f = forall x. x

unravel :: F Apply
unravel = unravel

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

In 4bdb10ca/ghc:

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.

comment:4 Changed 3 weeks ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T15664

Excellent point. Fixed now. Thanks!

comment:5 Changed 3 weeks ago by Iceland_jack

Description: modified (diff)

comment:6 Changed 3 weeks ago by Iceland_jack

Thanks

Note: See TracTickets for help on using tickets.