Core Lint error, from -fobject-code + defer type errors + pattern synonyms + other stuff
Try running this (-fobject-code is required) with and without -dcore-lint. I tried to minimize it but it is still hefty. This is showing it without -dcore-lint:
{-# Language RankNTypes, PatternSynonyms, DataKinds, PolyKinds, GADTs, TypeOperators, MultiParamTypeClasses, TypeFamilies, TypeSynonymInstances, FlexibleInstances, InstanceSigs, FlexibleContexts #-}
{-# Options_GHC -fdefer-type-errors #-}
import Data.Kind
import Data.Type.Equality
data TyVar :: Type -> Type -> Type where
VO :: TyVar (a -> as) a
VS :: TyVar as a -> TyVar (b -> as) a
data NP :: (k -> Type) -> ([k] -> Type) where
Nil :: NP f '[]
(:*) :: f a -> NP f as -> NP f (a:as)
data NS :: (k -> Type) -> ([k] -> Type) where
Here :: f a -> NS f (a:as)
There :: NS f as -> NS f (a:as)
infixr 6 :&:
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
data NA a
type SOP(kind::Type) code = NS (NP NA) code
data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where
AO :: a -> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
-> ApplyT(k -> ks) f (a:&:ctx)
from' :: ApplyT(Type -> Type -> Type) Either ctx -> NS (NP NA) '[ '[VO] ]
from' (ASSO (Left a)) = Here (a :* Nil)
from' (ASSO (Right b)) = There (Here undefined)
pattern ASSO
:: () =>
forall (ks :: Type) k (f :: k -> ks) (a1 :: k) (ks1 :: Type) k1 (f1 :: k1 -> ks1) (a2 :: k1) a3.
(kind ~ (k -> k1 -> Type), a ~~ f, b ~~ (a1 :&: a2 :&: E),
f a1 ~~ f1, f1 a2 ~~ a3) =>
a3 -> ApplyT kind a b
pattern ASSO a = AS (AS (AO a))$ ghci -ignore-dot-ghci -fobject-code 466.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 466.hs, 466.o )
466.hs:35:14: warning: [-Wdeferred-type-errors]
• Could not deduce: a2 ~ NA 'VO
from the context: ((* -> * -> *) ~ (k1 -> k2 -> *), Either ~~ f,
ctx ~~ (a2 ':&: (a3 ':&: 'E)), f a2 ~~ f1, f1 a3 ~~ a4)
bound by a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k -> ks) (a1 :: k) ks1 k1 (f1 :: k1
-> ks1) (a2 :: k1) a3.
(kind ~ (k -> k1 -> *), a ~~ f, b ~~ (a1 ':&: (a2 ':&: 'E)),
f a1 ~~ f1, f1 a2 ~~ a3) =>
a3 -> ApplyT kind a b,
in an equation for ‘from'’
at 466.hs:35:8-21
‘a2’ is a rigid type variable bound by
a pattern with pattern synonym:
ASSO :: forall kind (a :: kind) (b :: Ctx kind).
() =>
forall ks k (f :: k -> ks) (a1 :: k) ks1 k1 (f1 :: k1
-> ks1) (a2 :: k1) a3.
(kind ~ (k -> k1 -> *), a ~~ f, b ~~ (a1 ':&: (a2 ':&: 'E)),
f a1 ~~ f1, f1 a2 ~~ a3) =>
a3 -> ApplyT kind a b,
in an equation for ‘from'’
at 466.hs:35:8-21
Expected type: a4
Actual type: Either (NA 'VO) a3
• In the pattern: Left a
In the pattern: ASSO (Left a)
In an equation for ‘from'’: from' (ASSO (Left a)) = Here (a :* Nil)
• Relevant bindings include
from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]]
(bound at 466.hs:35:1)
|
35 | from' (ASSO (Left a)) = Here (a :* Nil)
| ^^^^^^^
466.hs:36:26: warning: [-Wdeferred-type-errors]
• Couldn't match type ‘a0 : as0’ with ‘'[]’
Expected type: NS (NP NA) '[ '[ 'VO]]
Actual type: NS (NP NA) ('[ 'VO] : a0 : as0)
• In the expression: There (Here undefined)
In an equation for ‘from'’:
from' (ASSO (Right b)) = There (Here undefined)
• Relevant bindings include
from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]]
(bound at 466.hs:35:1)
|
36 | from' (ASSO (Right b)) = There (Here undefined)
| ^^^^^^^^^^^^^^^^^^^^^^
WARNING: file compiler/types/TyCoRep.hs, line 2378
in_scope InScope {wild_00 wild_Xl wild_Xv wild_X1m a_a1Gv ks_a1Ou
k_a1Ov f_a1Ow a_a1Ox ctx_a1Oy co_a1Oz co_a1OA co_a1OB ks_a1OC
k_a1OD f_a1OE a_a1OF ctx_a1OG co_a1OH co_a1OI co_a1OJ a_a1OK
co_a1OL co_a1OM co_a1ON as_a1Q3 a_a1Q4 ctx_a1Q5 $krep_a2XW
$krep_a2XX $krep_a2XY $krep_a2XZ $krep_a2Y0 $krep_a2Y1 $krep_a2Y2
$krep_a2Y3 $krep_a2Y4 $krep_a2Y5 $krep_a2Y6 $krep_a2Y7 $krep_a2Y8
$krep_a2Y9 $krep_a2Ya $krep_a2Yb $krep_a2Yc $krep_a2Yd $krep_a2Ye
$krep_a2Yf $krep_a2Yg $krep_a2Yh $krep_a2Yi $krep_a2Yj $krep_a2Yk
$krep_a2Yl $krep_a2Ym $krep_a2Yn $krep_a2Yo $krep_a2Yp $krep_a2Yq
$krep_a2Yr $krep_a2Ys $krep_a2Yt $krep_a2Yu $krep_a2Yv $krep_a2Yw
$krep_a2Yx $krep_a2Yy $krep_a2Yz $krep_a2YA $krep_a2YB $krep_a2YC
$krep_a2YD $krep_a2YE $krep_a2YF $krep_a2YG $krep_a2YH $krep_a2YI
$krep_a2YJ $krep_a2YK $krep_a2YL ds_d2YO ds_d2YP ds_d2YV fail_d2Z2
from' $bASSO $mASSO $tc':&: $tc':* $tc'AO $tc'AS $tc'E $tc'Here
$tc'Nil $tc'There $tc'VO $tc'VS $tcApplyT $tcCtx $tcNA $tcNP $tcNS
$tcTyVar $trModule $trModule_s2ZM $trModule_s2ZN $trModule_s2ZO
$trModule_s2ZP $krep_s2ZQ $krep_s2ZR $krep_s2ZS $krep_s2ZT
$krep_s2ZU $krep_s2ZV $krep_s2ZW $krep_s2ZX $tcTyVar_s2ZY
$tcTyVar_s2ZZ $krep_s300 $krep_s301 $krep_s302 $krep_s303
$tc'VO_s304 $tc'VO_s305 $krep_s306 $krep_s307 $tc'VS_s308
$tc'VS_s309 $tcNP_s30a $tcNP_s30b $krep_s30c $krep_s30d $krep_s30e
$krep_s30f $krep_s30g $krep_s30h $tc':*_s30i $tc':*_s30j $krep_s30k
$krep_s30l $krep_s30m $tc'Nil_s30n $tc'Nil_s30o $tcNS_s30p
$tcNS_s30q $krep_s30r $krep_s30s $krep_s30t $krep_s30u $krep_s30v
$krep_s30w $tc'Here_s30x $tc'Here_s30y $krep_s30z $krep_s30A
$krep_s30B $tc'There_s30C $tc'There_s30D $tcCtx_s30E $tcCtx_s30F
$krep_s30G $krep_s30H $krep_s30I $tc':&:_s30J $tc':&:_s30K
$krep_s30L $krep_s30M $krep_s30N $krep_s30O $krep_s30P $tc'E_s30Q
$tc'E_s30R $tcNA_s30S $tcNA_s30T $tcApplyT_s30U $tcApplyT_s30V
$krep_s30W $krep_s30X $krep_s30Y $krep_s30Z $krep_s310 $krep_s311
$tc'AS_s312 $tc'AS_s313 $krep_s314 $krep_s315 $krep_s316
$tc'AO_s317 $tc'AO_s318}
tenv [a1Ow :-> f_a1Ow, a1Ox :-> a_a1Ox, a1Oy :-> ctx_a1Oy,
a1OE :-> f_a1OE, a1OF :-> a_a1OF, a1OG :-> ctx_a1OG]
cenv [a1Oz :-> co_a1Oz, a1OA :-> co_a1OA, a1OB :-> co_a1OB,
a1OH :-> co_a1OH, a1OI :-> co_a1OI, a1OJ :-> co_a1OJ,
a1OL :-> co_a1OL, a1OM :-> co_a1OM, a1ON :-> co_a1ON]
tys [a_a1Ox ~# (NA 'VO |> Sym (Nth:2 (Sym co_a2U0)))]
cos []
needInScope [a1Ov :-> k_a1Ov, a1OD :-> k_a1OD, a1Q3 :-> as_a1Q3,
a1Q4 :-> a_a1Q4, a2U0 :-> co_a2U0]
WARNING: file compiler/types/TyCoRep.hs, line 2378
in_scope InScope {wild_00 wild_Xl wild_Xv wild_X1m a_a1Gv ks_a1Ou
k_a1Ov f_a1Ow a_a1Ox ctx_a1Oy co_a1Oz co_a1OA co_a1OB ks_a1OC
k_a1OD f_a1OE a_a1OF ctx_a1OG co_a1OH co_a1OI co_a1OJ a_a1OK
co_a1OL co_a1OM co_a1ON as_a1Q3 a_a1Q4 ctx_a1Q5 $krep_a2XW
$krep_a2XX $krep_a2XY $krep_a2XZ $krep_a2Y0 $krep_a2Y1 $krep_a2Y2
$krep_a2Y3 $krep_a2Y4 $krep_a2Y5 $krep_a2Y6 $krep_a2Y7 $krep_a2Y8
$krep_a2Y9 $krep_a2Ya $krep_a2Yb $krep_a2Yc $krep_a2Yd $krep_a2Ye
$krep_a2Yf $krep_a2Yg $krep_a2Yh $krep_a2Yi $krep_a2Yj $krep_a2Yk
$krep_a2Yl $krep_a2Ym $krep_a2Yn $krep_a2Yo $krep_a2Yp $krep_a2Yq
$krep_a2Yr $krep_a2Ys $krep_a2Yt $krep_a2Yu $krep_a2Yv $krep_a2Yw
$krep_a2Yx $krep_a2Yy $krep_a2Yz $krep_a2YA $krep_a2YB $krep_a2YC
$krep_a2YD $krep_a2YE $krep_a2YF $krep_a2YG $krep_a2YH $krep_a2YI
$krep_a2YJ $krep_a2YK $krep_a2YL ds_d2YO ds_d2YP ds_d2YV fail_d2Z2
from' $bASSO $mASSO $tc':&: $tc':* $tc'AO $tc'AS $tc'E $tc'Here
$tc'Nil $tc'There $tc'VO $tc'VS $tcApplyT $tcCtx $tcNA $tcNP $tcNS
$tcTyVar $trModule $trModule_s2ZM $trModule_s2ZN $trModule_s2ZO
$trModule_s2ZP $krep_s2ZQ $krep_s2ZR $krep_s2ZS $krep_s2ZT
$krep_s2ZU $krep_s2ZV $krep_s2ZW $krep_s2ZX $tcTyVar_s2ZY
$tcTyVar_s2ZZ $krep_s300 $krep_s301 $krep_s302 $krep_s303
$tc'VO_s304 $tc'VO_s305 $krep_s306 $krep_s307 $tc'VS_s308
$tc'VS_s309 $tcNP_s30a $tcNP_s30b $krep_s30c $krep_s30d $krep_s30e
$krep_s30f $krep_s30g $krep_s30h $tc':*_s30i $tc':*_s30j $krep_s30k
$krep_s30l $krep_s30m $tc'Nil_s30n $tc'Nil_s30o $tcNS_s30p
$tcNS_s30q $krep_s30r $krep_s30s $krep_s30t $krep_s30u $krep_s30v
$krep_s30w $tc'Here_s30x $tc'Here_s30y $krep_s30z $krep_s30A
$krep_s30B $tc'There_s30C $tc'There_s30D $tcCtx_s30E $tcCtx_s30F
$krep_s30G $krep_s30H $krep_s30I $tc':&:_s30J $tc':&:_s30K
$krep_s30L $krep_s30M $krep_s30N $krep_s30O $krep_s30P $tc'E_s30Q
$tc'E_s30R $tcNA_s30S $tcNA_s30T $tcApplyT_s30U $tcApplyT_s30V
$krep_s30W $krep_s30X $krep_s30Y $krep_s30Z $krep_s310 $krep_s311
$tc'AS_s312 $tc'AS_s313 $krep_s314 $krep_s315 $krep_s316
$tc'AO_s317 $tc'AO_s318}
tenv [a1Ow :-> f_a1Ow, a1Ox :-> a_a1Ox, a1Oy :-> ctx_a1Oy,
a1OE :-> f_a1OE, a1OF :-> a_a1OF, a1OG :-> ctx_a1OG]
cenv [a1Oz :-> co_a1Oz, a1OA :-> co_a1OA, a1OB :-> co_a1OB,
a1OH :-> co_a1OH, a1OI :-> co_a1OI, a1OJ :-> co_a1OJ,
a1OL :-> co_a1OL, a1OM :-> co_a1OM, a1ON :-> co_a1ON]
tys [a_a1Ox ~# (NA 'VO |> Sym (Nth:2 (Sym co_a2U0)))]
cos []
needInScope [a1Ov :-> k_a1Ov, a1OD :-> k_a1OD, a1Q3 :-> as_a1Q3,
a1Q4 :-> a_a1Q4, a2U0 :-> co_a2U0]
Ok, one module loaded.
Prelude Main>