Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Register
  • Sign in
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
    • Locked files
  • Issues 5.5k
    • Issues 5.5k
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 631
    • Merge requests 631
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
    • Test cases
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #15695

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> 
Edited Mar 10, 2019 by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking