#15796 closed bug (fixed)

Core Lint error with invalid newtype declaration

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.2
Component: Compiler (Type checker) Version: 8.6.1
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: typecheck/should_fail/T15796
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This gives a Core Lint error

{-# Language QuantifiedConstraints #-}
{-# Language TypeApplications      #-}
{-# Language TypeOperators         #-}
{-# Language PolyKinds             #-}
{-# Language FlexibleInstances     #-}
{-# Language DataKinds             #-}
{-# Language TypeFamilies          #-}
{-# Language MultiParamTypeClasses #-}
{-# Language ConstraintKinds       #-}
{-# Language UndecidableInstances  #-}
{-# Language GADTs                 #-}

{-# Options_GHC -dcore-lint #-}

import Data.Kind

type Cat ob = ob -> ob -> Type

class Ríki (obj :: Type) where
  type (-->) :: Cat obj

class Varpi (f :: dom -> cod)

newtype
  (··>) :: Cat (a -> b) where
  Natu :: Varpi f
       => (forall xx. f xx --> f' xx)
       -> (f ··> f')

instance
     Ríki cod
  => -------------
     Ríki (dom -> cod)
  where

  type (-->) = (··>) @dom @cod
$ ghci -ignore-dot-ghci 568_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 568_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20181017 for x86_64-unknown-linux):
        Core Lint error
  <no location info>: warning:
      In the type ‘(··>)’
      Found TcTyCon: ··>[tc]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

> :q
Leaving GHCi.

Change History (10)

comment:1 Changed 11 months ago by simonpj

Keywords: TypeApplications added

This is related to Visible Kind Application, correct? Which is not yet committed to HEAD?

comment:2 Changed 11 months ago by goldfire

Cc: mnguyen added
Summary: Core Lint errorCore Lint error with visible kind application

Yes.

comment:3 Changed 11 months ago by Iceland_jack

Yes it is Simon this uses D5229 (Visible kind application). Here is another program that triggers a similar error

{-# Language DataKinds             #-}
{-# Language TypeOperators         #-}
{-# Language PolyKinds             #-}
{-# Language GADTs                 #-}
{-# Language TypeFamilies          #-}

{-# Options_GHC -dcore-lint #-}

import qualified GHC.TypeLits as TypeLits
import Data.Kind

data OP a = Op a

type family
 UnOp (op_a :: OP a) :: a where
 UnOp (Op a) = a

class Ríki (obj :: Type) where
 type (-->) :: OP obj -> obj -> Type

data (<=) :: OP TypeLits.Nat -> TypeLits.Nat -> Type where
  LessThan :: TypeLits.KnownNat (UnOp op_a)
           => op_a <= b

instance Ríki TypeLits.Nat where
 type (-->) = (<=)
$ ghci -ignore-dot-ghci 572_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 572_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20181017 for x86_64-unknown-linux):
        Core Lint error
  <no location info>: warning:
      In the type ‘(<=)’
      Found TcTyCon: <=[tc]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

>

comment:4 Changed 11 months ago by goldfire

Cc: mnguyen removed
Keywords: TypeInType added; TypeApplications removed

Can be triggered without visible kind application:

{-# Language QuantifiedConstraints #-}
{-# Language TypeApplications      #-}
{-# Language TypeOperators         #-}
{-# Language PolyKinds             #-}
{-# Language FlexibleInstances     #-}
{-# Language DataKinds             #-}
{-# Language TypeFamilies          #-}
{-# Language MultiParamTypeClasses #-}
{-# Language ConstraintKinds       #-}
{-# Language UndecidableInstances  #-}
{-# Language GADTs                 #-}

{-# Options_GHC -dcore-lint #-}

import Data.Kind

type Cat ob = ob -> ob -> Type

class Ríki (obj :: Type) where
  type (-->) :: Cat obj

class Varpi (f :: dom -> cod)

newtype
  (··>) :: Cat (a -> b) where
  Natu :: Varpi f
       => (forall xx. f xx --> f' xx)
       -> (f ··> f')

instance
     Ríki cod
  => -------------
     Ríki (dom -> cod)
  where

  type (-->) = ((··>) :: Cat (dom -> cod))

comment:5 Changed 11 months ago by RyanGlScott

Component: CompilerCompiler (Type checker)
Keywords: TypeFamilies added; TypeInType removed
Milestone: 8.8.1
Summary: Core Lint error with visible kind applicationCore Lint error with invalid newtype declaration
Type of failure: None/UnknownCompile-time crash or panic

Even simpler example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

newtype N a where
  MkN :: Show a => a -> N a
type family T a
type instance T (N a) = N a
$ /opt/ghc/8.6.1/bin/ghci Bug.hs -dcore-lint
GHCi, version 8.6.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.1 for x86_64-unknown-linux):
        Core Lint error
  <no location info>: warning:
      In the type ‘N a_a1P7’
      Found TcTyCon: N[tc]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst

The culprit appears to be the invalid Show a context in the MkN newtype constructor, as removing that makes the Core Lint error go away.

Note that this only happens in GHC 8.6.1 and later. In earlier versions of GHC, this simply gives an error message:

$ /opt/ghc/8.4.4/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:6:3: error:
    • A newtype constructor cannot have a context in its type
      MkN :: forall a. Show a => a -> N a
    • In the definition of data constructor ‘MkN’
      In the newtype declaration for ‘N’
  |
6 |   MkN :: Show a => a -> N a
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^

comment:6 Changed 11 months ago by goldfire

I'm pretty sure I know what's happening:

  • The newtype declaration is bogus. It kind-checks, but then fails the validity check.
  • If a declaration fails a validity check, we manufacture a "recovery tycon", which is a TcTyCon. See Note [Recover from validity error] in TcTyClsDecls.
  • When we create a type family instance, we (optionally) do a quick core-lint check on it, as there's no other time we ever do so.
  • Core lint falls over when it sees a TcTyCon, which should never make it past the type checker.

I don't want to remove this last check. And I don't want to abolish recovery tycons, as they produce nice error messages. Maybe we tell core-lint (in a new parameter) that it's being called in the type checker? Maybe we skip this check if there are errors? Yes, that seems sensible. Patch incoming.

comment:7 Changed 11 months ago by Richard Eisenberg <rae@…>

In 1f72a1c8/ghc:

Don't lint erroneous programs.

newFamInst lints its types. This is good. But it's not so good
when there have been errors and thus recovery tycons are about.
So we now don't.

Fixes #15796.

Test case: typecheck/should_fail/T15796

comment:8 Changed 11 months ago by goldfire

Status: newmerge
Test Case: typecheck/should_fail/T15796

This is easy to merge.

comment:9 Changed 11 months ago by RyanGlScott

Milestone: 8.8.18.6.2

comment:10 Changed 10 months ago by bgamari

Resolution: fixed
Status: mergeclosed

This was merged for 8.6.2 in 41f0f6c2f571ea05c49f9f6ed64beebdc5a9f9fc.

Note: See TracTickets for help on using tickets.