#14607 closed bug (fixed)

Core Lint error

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.2
Keywords: TypeInType, DeferredTypeErrors Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T14607
Blocked By: Blocking:
Related Tickets: #14605 #14584 Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

This produces a long Core lint error:

{-# Language DerivingStrategies #-}
{-# Language GADTs #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs #-}
{-# Language KindSignatures #-}
{-# Language TypeFamilies #-}
{-# Language TypeInType #-}
{-# Language TypeOperators #-}

import Data.Kind

data DEFUNC :: Type -> Type -> Type where
  (:~>) :: a -> b -> DEFUNC a b

type a ~> b = DEFUNC a b -> Type
    
data LamCons a :: Type ~> Type where
  LamCons :: a -> LamCons a ([a] :~> [a])

class Mk (app :: Type ~> Type) where
  type Arg app :: Type

  mk :: Arg app -> app (a :~> b)

instance Mk (LamCons a :: Type ~> Type) where
  type Arg (LamCons a) = a

  mk :: a -> LamCons (a :~> b)
  mk = LamCons

with ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint bug.hs on GHC 8.2.1 and 8.3.20171208.

Change History (5)

comment:1 Changed 10 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 10 months ago by Iceland_jack

Simplified example

{-# Language GADTs #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs #-}
{-# Language KindSignatures #-}
{-# Language TypeInType #-}

import Data.Kind

type Arr = (Type, Type) -> Type
    
data LamCons a :: Arr where
  LamCons :: LamCons a '(a, a)

class Mk (app :: Arr) where
  mk :: app '(a, b)

instance Mk (LamCons a :: Arr) where
  mk :: LamCons '(a, b)
  mk = undefined

Changing last '(a, b) to '(a, a) makes it not crash.

Also fails with type-level lists / Maybe: same cause?

type Arr'  = [Type]     -> Type
type Arr'' = Maybe Type -> Type
    
data LamCons'  a :: Arr'  where LamCons'  :: LamCons'  a '[a, a]
data LamCons'' a :: Arr'' where LamCons'' :: LamCons'' a ('Just (a, a))

class Mk'  (app'  :: Arr')  where mk'  :: app'  '[]
class Mk'' (app'' :: Arr'') where mk'' :: app'' 'Nothing

instance Mk'  (LamCons'  a :: Arr')  where mk'  :: LamCons'  '[a, b];        mk'  = undefined
instance Mk'' (LamCons'' a :: Arr'') where mk'' :: LamCons'' ('Just (a, b)); mk'' = undefined
Last edited 10 months ago by Iceland_jack (previous) (diff)

comment:3 Changed 10 months ago by monoidal

Small simplification:

{-# Language GADTs #-}
{-# Language InstanceSigs #-}
{-# Language KindSignatures #-}
{-# Language TypeFamilies #-}
{-# Language DataKinds #-}
{-# Language FlexibleInstances #-}

import Data.Kind

data LamCons :: Type -> Type -> () -> Type where
  C :: LamCons a a '()

class Mk a where
  mk :: LamCons a a '()

instance Mk a where
  mk :: LamCons a '()
  mk = mk

comment:4 Changed 10 months ago by Simon Peyton Jones <simonpj@…>

In 9e5535ca/ghc:

Fix OptCoercion

In the presence of -fdefer-type-errors, OptCoercion can
encounter a mal-formed coerercion with type
    T a ~ T a b
and that was causing a subsequent Lint error.

This caused Trac #14607.  Easily fixed by turning an ASSERT
into a guard.

comment:5 Changed 10 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T14607
Note: See TracTickets for help on using tickets.