[GHC] #15695: Core Lint error, from -fobject-code + defer type errors + pattern synonyms + other stuff

30 Sep 2018


      #15695: Core Lint error, from -fobject-code + defer type errors + pattern synonyms
+ other stuff
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.6.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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`:

 {{{#!hs
 {-# 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))
 }}}

 {{{
 $ latestbug -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>
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15695
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler