Opened 4 weeks ago

Closed 2 weeks ago

#14605 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/T14605
Blocked By: Blocking:
Related Tickets: #14584 Differential Rev(s):
Wiki Page:


This piece of code fails when run with ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint bug.hs, maybe same as my previous #14584.

{-# Language DerivingStrategies #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
{-# Language TypeInType #-}
{-# Language TypeOperators #-}
{-# Language UndecidableInstances #-}

import Data.Kind
import Data.Functor.Identity
import Data.Functor.Product

type a <-> b = a -> b -> Type

class Iso (iso :: a <-> b) where
  iso :: a -> b
  osi :: b -> a

data Iso_Bool :: Either () () <-> Bool

instance Iso Iso_Bool where

class Representable f where
  type Rep f :: Type

  index    :: f a -> (Rep f -> a)
  tabulate :: (Rep f -> a) -> f a

class Comonad w where
  extract   :: w a -> a
  duplicate :: w a -> w (w a)

newtype Co f a = Co (f a) deriving newtype (Functor, Representable)

instance (Representable f, Monoid (Rep f)) => Comonad (Co f) where
  extract = (`index` mempty)

newtype WRAP (iso::old <-> new) f a = WRAP (f a)

instance (Representable f, Rep f ~ old, Iso iso) => Representable (WRAP (iso :: old <-> new) f) where
  type Rep (WRAP (iso :: old <-> new) f) = new

  index :: WRAP iso f a -> (new -> a)
  index (WRAP fa) = index fa . osi @old @new @iso

  tabulate :: (new -> a) -> WRAP iso f a
  tabulate gen = WRAP $ 
    tabulate (gen . iso @old @new @iso)

newtype PAIR a = PAIR (Co (WRAP Iso_Bool (Product Identity Identity)) a)
  deriving newtype

I unfortunately don't have time to find a more minimal example. Core linter vomits a lot of errors on 8.2.1 & 8.3.20171208.

Change History (7)

comment:1 Changed 4 weeks ago by Iceland_jack

comment:2 Changed 4 weeks ago by monoidal

Similar to #14584. The essence is the code that is generated via GND for Comonad PAIR, which I've reduced to:

{-# Language TypeApplications #-}
{-# Language ImpredicativeTypes #-}

import GHC.Prim (coerce)

duplicate = coerce @(forall x. ()) @(forall x. x)

(though it's possible there are more factors causing the bug and I isolated only one of them)

comment:3 Changed 4 weeks ago by simonpj

The error is a kind error under a forall type, which gets an implication constraint, but with nowhere to put its (value) bindings. The the deferred type error produces a value binding that is then discarded.

Monoidal, you are brilliant at reducing these examples to their essence. Amazing.

comment:4 Changed 4 weeks ago by Iceland_jack

Thanks monoidal for cleaning up my mess :)

comment:5 Changed 2 weeks ago by simonpj

Richard and I decided that the simple way to do this is to switch off deferred type errors when inside a forall-unification.

One could also imagine using the enclosing value bindings, but the necessary variables won't be in scope there.

We could instead bind a bogus coercion in the outside scope, with a vanilla type like () ~ () and then unsafe-corece it to the one we need. But it's more complicated and doesn't seem with the pain unless we get user pressure.

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

In 298ec78c/ghc:

No deferred type errors under a forall

As Trac #14605 showed, we can't defer a type error under a
'forall' (when unifying two forall types).

The fix is simple.

comment:7 Changed 2 weeks ago by simonpj

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