Core Lint errors : from quantification in Dict
Maybe an old bug. On GHC 8.10.0.20191123:
{-# Language ConstraintKinds #-}
{-# Language GADTs #-}
{-# Language ImpredicativeTypes #-}
{-# Options_GHC -dcore-lint #-}
data Dict cls where
Dict :: cls => Dict cls
x :: Dict (forall a. Functor (bi a))
x = Dict
produces
$ ghci ~/hs/5781.hs
GHCi, version 8.10.0.20191123: https://www.haskell.org/ghc/ :? for help
Loaded package environment from /home/baldur/.ghc/x86_64-linux-8.10.0.20191123/environments/default
[1 of 1] Compiling Main ( /home/baldur/hs/5781.hs, interpreted )
*** Core Lint errors : in result of Desugar (before optimization) ***
/home/baldur/hs/5781.hs:10:1: warning:
Out of scope: irred_aBN :: cls_aBM[tau:1]
[LclId]
In the RHS of x :: forall (bi :: * -> * -> *).
Dict (forall a. Functor (bi a))
In the body of lambda with binder bi_aBK :: * -> * -> *
Substitution: [TCvSubst
In scope: InScope {bi_aBK $krep_aC7 $krep_aC8 $krep_aC9 $krep_aCa
$krep_aCb x $tc'Dict $tcDict $trModule}
Type env: []
Co env: []]
*** Offending Program ***
Rec {
$tcDict :: TyCon
[LclIdX]
$tcDict
= TyCon
12987113738476613843##
8633772289720193919##
$trModule
(TrNameS "Dict"#)
0#
$krep_aC7
$tc'Dict :: TyCon
[LclIdX]
$tc'Dict
= TyCon
2488727520366487455##
14348606358165608576##
$trModule
(TrNameS "'Dict"#)
1#
$krep_aC9
$krep_aC9 [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aC9 = KindRepFun $krep_aCa $krep_aCb
$krep_aC7 [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aC7 = KindRepFun $krep_aC8 krep$*
$krep_aCb [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aCb
= KindRepTyConApp $tcDict (: @ KindRep $krep_aCa ([] @ KindRep))
$krep_aC8 [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aC8 = KindRepTyConApp $tcConstraint ([] @ KindRep)
$krep_aCa [InlPrag=NOUSERINLINE[~]] :: KindRep
[LclId]
$krep_aCa = $WKindRepVar (I# 0#)
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Main"#)
x :: forall (bi :: * -> * -> *). Dict (forall a. Functor (bi a))
[LclIdX]
x = \ (@ (bi_aBK :: * -> * -> *)) ->
break<0>() Dict @ (forall a. Functor (bi_aBK a)) irred_aBN
end Rec }
*** End of Offense ***
<no location info>: error:
Compilation had errors
*** Exception: ExitFailure 1
Before shrinking:
Click this to collapse/fold.
import Prelude hiding (Functor(..), id, (.))
import Data.Proxy
import Prelude qualified
import Control.Category
import Data.Kind
import Data.Bifunctor
type Cat :: Type -> Type
type Cat ob = ob -> ob -> Type
type Functor :: (s -> t) -> Constraint
class (Category (Source f), Category (Target f)) => Functor (f :: s -> t) where
type Source (f :: s -> t) :: Cat s
type Target (f :: s -> t) :: Cat t
fmap :: Source f a a' -> Target f (f a) (f a')
type FunctorOf :: Cat s -> Cat t -> (s -> t) -> Constraint
class (Functor f, Source f ~ src, Target f ~ tgt) => FunctorOf src tgt f
instance (Functor f, Source f ~ src, Target f ~ tgt) => FunctorOf src tgt f
type Nat :: Cat s -> Cat t -> Cat (s -> t)
data Nat src tgt f f' where
NatId
:: Nat src tgt f f
Nat
:: (FunctorOf src tgt f, FunctorOf src tgt f')
=> (forall a. tgt (f a) (f' a))
-> Nat src tgt f f'
instance (Category src, Category tgt) => Category (Nat src tgt) where
id :: Nat src tgt f f
id = NatId
(.) :: Nat src tgt g h -> Nat src tgt f g -> Nat src tgt f h
Nat f . Nat g = Nat (f . g)
instance Functor (,) where
type Source (,) = (->)
type Target (,) = Nat (->) (->)
fmap :: (a -> a') -> Nat (->) (->) ((,) a) ((,) a')
fmap f = Nat (first f)
instance Functor ((,) a) where
type Source ((,) a) = (->)
type Target ((,) a) = (->)
fmap :: (b -> b') -> ((a, b) -> (a, b'))
fmap = second
type Dict :: Constraint -> Type
data Dict cls where
Dict :: cls => Dict cls
wit :: forall bi. ()
=> FunctorOf (->) (Nat (->) (->)) bi
=> (forall a. Nat (->) (->) (bi a) (bi a))
-> Dict (forall a. FunctorOf (->) (->) (bi a))
wit (Nat nat)
| let
x :: Dict (forall a. FunctorOf (->) (->) (bi a))
x = Dict
= undefined
foo :: FunctorOf src1 (Nat src2 tgt) bi => forall a. Nat src2 tgt (bi a) (bi a)
foo = fmap id
foo' :: forall s (src1 :: Cat s) src2 tgt bi. ()
=> FunctorOf src1 (Nat src2 tgt) bi
=> forall a. Proxy a -> Dict (FunctorOf src2 tgt (bi a))
foo' (Proxy :: _ a) = case foo @src1 @src2 @tgt @bi @a of
Nat nat -> Dict :: Dict (FunctorOf src2 tgt (bi a))