Opened 2 years ago

Last modified 16 months ago

#13547 new bug

Lint error in arrows program

Reported by: cipher1024 Owned by:
Priority: normal Milestone:
Component: Compiler (CodeGen) Version: 8.0.1
Keywords: Arrows Cc: Henrik.Nilsson@…, Ross, Paterson, <ross@…>
Operating System: Unknown/Multiple Architecture: x86_64 (amd64)
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: #5777, #10158, #15175 Differential Rev(s):
Wiki Page:

Description (last modified by cipher1024)

When building with stack build --resolver lts-7.20and stack build --resolver lts-8.8, i.e. with ghc-8.0.1 and ghc-8.0.2.

    [37 of 60] Compiling Document.Phase.Proofs ( src/Document/Phase/Proofs.hs, .stack-work/dist/x86_64-osx/Cabal-1.24.0.0/build/Document/Phase/Proofs.o )
    
    <no location info>: error:
        ghc: panic! (the 'impossible' happened)
      (GHC version 8.0.1 for x86_64-apple-darwin):
    	StgCmmEnv: variable not found
      $dTypeable_aZSM
      local binds for:
      $sunionWith_$sunionWithKey
      $sfromList1
      $sfromList3
      $sfromList
      $s$fOrdEither
      $s$fMonadReaderrReaderT
      $s$fIsTupleconstrIdentity
      $s$fIsTupleconstr(,,,,)
      $s$fIsTupleconstr(,,,)
      $s$fIsTupleconstr(,,)
      $s$fIsTupleconstr(,,)2
      $s$fIsTupleconstr(,)1
      $s$fIsTupleconstr(,)
      $s$fIsTupleconstr(,)2
      $s$fHasMachineP2p
      $fNFDataEventRefA
      $fMonoidEventRefA
      $fGenericEventRefA
      $wmake_phase4
      make_phase1
      $wpoly_go10
      make_phase2
      make_phase3
      make_phase5
      $fNFDataEventRefA4
      $fNFDataEventRefA2
      $stypeRep#78
      $swithCommand8
      $stypeRep#54
      $swithCommand5
      $stypeRep#11
      $swithCommand2
      $stypeRep#74
      $stypeRep#81
      $stypeRep#15
      $stypeRep#20
      $stypeRep#79
      $stypeRep#80
      $stypeRep#70
      $stypeRep#75
      $stypeRep#58
      $stypeRep#66
      $stypeRep#71
      $stypeRep#62
      $stypeRep#8
      $stypeRep#67
      $stypeRep#63
      $stypeRep#59
      $stypeRep#50
      $stypeRep#55
      $stypeRep#38
      $stypeRep#46
      $stypeRep#51
      $stypeRep#42
      $stypeRep#47
      $stypeRep#43
      $stypeRep#34
      $stypeRep#39
      $stypeRep#31
      $stypeRep#35
      $stypeRep#28
      $stypeRep#24
      $stypeRep#25
      $stypeRep#21
      $stypeRep#3
      $stypeRep#16
      $stypeRep#7
      $stypeRep#12
      $stypeRep#2
      $smakeCell8
      $smakeCell7
      $smakeCell40
      $smakeCell39
      $smakeCell36
      $smakeCell35
      $smakeCell32
      $smakeCell31
      $smakeCell4
      $smakeCell28
      $smakeCell27
      $smakeCell24
      $smakeCell23
      $smakeCell3
      $smakeCell20
      $smakeCell19
      $smakeCell16
      $smakeCell15
      $smakeCell12
      $smakeCell11
      $wpoly_go5
      $wgo5
      $sfromList_go5
      $wpoly_go2
      $sfromList2
      $s$fOrd(,)
      $sfromList_fromList'1
      $wpoly_go1
      $s$fEqEither
      $s$fOrdEither_$s$fOrdEither_$cp1Ord
      $s$fEq(,)
      $s$fOrd(,)_$s$fOrd(,)_$cp1Ord
      $s$fMonadRWST
      $s$fMonadReaderrReaderT1
      $s$fMonadReaderT
      $s$fApplicativeReaderT
      $s$fMonadReaderT_$s$fMonadReaderT_$cfail
      $s$fMonadReaderT_$s$fMonadReaderT_$c>>
      $s$fMonadReaderT_$s$fMonadReaderT_$c>>=
      $s$fMonadReaderT_$s$fMonadReaderT_$cp1Monad
      $s$fMonadRWST_$s$fMonadRWST_$cfail
      $s$fMonadRWST_$s$fMonadRWST_$c>>
      $s$fMonadRWST_$s$fMonadRWST_$c>>=
      $s$fMonadRWST_$s$fMonadRWST_$cp1Monad
      $s$fIsTupleconstr(,,,,)_$s$fLatexArg[]
      $s$fIsTupleconstr(,,,,)1
      $s$fIsTupleconstr(,,,)_$s$fLatexArg[]
      $s$fIsTupleconstr(,,,)_irred2
      $s$fIsTupleconstr(,,)_$s$fLatexArg[]
      $s$fIsTupleconstr(,,)_$dLatexArgFromString
      $s$fIsTupleconstr(,,)_$s$fLatexArgFromStringConc
      $s$fIsTupleconstr(,,)_irred1
      $s$fIsTupleconstr(,,)_$s$fLatexArgNonEmpty
      $s$fIsTupleconstr(,,)1
      $s$fIsTupleconstr(,)3
      $s$fHasMachineP1p
      $s$fHasMachineP2p1
      $s$fHasMachineP2p2
      $s$fHasMachineP2p3
      $s$fHasMachineP2p4
      $s$fHasMachineP2p5
      $s$fHasMachineP2p6
      $s$fHasMachineP1p_$s$fHasMachineP1p_$cp5HasMachineP1
      $s$fHasMachineP1p_$s$fHasMachineP1p_$cp4HasMachineP1
      $s$fHasMachineP1p_$s$fHasMachineP1p_$cp3HasMachineP1
      $s$fHasMachineP1p_$s$fHasMachineP1p_$cp2HasMachineP1
      $s$fHasMachineP1p_$s$fHasMachineP1p_$cp1HasMachineP1
      $s$fEq(,)_$dEq1
      $s$fEq(,)_$dEq
      $s$fApplicativeReaderT_$s$fFunctorReaderT_$c<$
      $s$fApplicativeReaderT_$s$fFunctorReaderT_$cfmap
      $s$fApplicativeReaderT_$s$fFunctorReaderT
      $s$fApplicativeRWST
      $s$fApplicativeReaderT_$dApplicative
      $s$fApplicativeReaderT_$s$fApplicativeReaderT_$c<*>
      $s$fApplicativeReaderT_$s$fMonadReaderT_$creturn
      $s$fApplicativeReaderT_$s$fApplicativeReaderT_$cp1Applicative
      $s$fApplicativeRWST_$dFunctor
      $s$fApplicativeRWST_$s$fApplicativeRWST_$c<*>
      $s$fApplicativeRWST_$s$fApplicativeRWST_$cpure
      $s$fApplicativeRWST_$s$fApplicativeRWST_$cp1Applicative
      $fNFDataEventRefA1
      $fNFDataEventRefA3
      $w$dNFData2
      $w$dNFData1
      $w$dNFData
      $fNFDataEventRefA_$crnf
      $wgo
      $fMonoidEventRefA_$cmconcat
      $fMonoidEventRefA_$cmappend
      $fMonoidEventRefA_$cmempty
      $fGenericEventRefA_$cto
      $fGenericEventRefA_$cfrom
      make_phase4
      ruleProxies_rSKY
      refinement_parser_rSL2
      $w$smiddle
      $w$sgreater
      $sfilterGt1
      $sfilterLt1
      $sinsert_$sgo10
      $sinsert_$sgo5
      $sleadsTo1
      $wpoly_go3
      $wpoly_go4
      $slookup5
      $slookup7
      $smakeCell2
      $smakeCell6
      $smakeCell10
      $smakeCell14
      $smakeCell18
      $smakeCell22
      $smakeCell26
      $smakeCell30
      $smakeCell34
      $smakeCell38
      $wpoly_go6
      $wpoly_go7
      $wpoly_go8
      $sshowStringP1
      $strim1
      $strim3
      $sunions1
      $sunless_eta
      $swithCommand1
      $swithCommand4
      $swithCommand7
      lvl_r2714
      lvl1_r2715
      go_r2716
      $wgo1_r2717
      lvl2_r2718
      lvl3_r2719
      lvl4_r271a
      lvl5_r271b
      lvl6_r271c
      lvl7_r271d
      lvl8_r271e
      lvl9_r271f
      lvl10_r271g
      lvl11_r271h
      lvl12_r271i
      lvl13_r271j
      lvl14_r271k
      lvl15_r271l
      lvl16_r271m
      lvl17_r271n
      lvl18_r271o
      lvl19_r271p
      lvl20_r271q
      lvl21_r271r
      lvl22_r271s
      lvl23_r271t
      lvl24_r271u
      lvl25_r271v
      lvl26_r271w
      lvl27_r271x
      lvl28_r271y
      lvl29_r271z
      lvl30_r271A
      lvl31_r271B
      lvl32_r271C
      lvl33_r271D
      lvl34_r271E
      lvl35_r271F
      lvl36_r271G
      lvl37_r271H
      lvl38_r271I
      lvl39_r271J
      lvl40_r271K
      lvl49_r2723
      lvl50_r2724
      lvl51_r2725
      lvl52_r2726
      lvl53_r2727
      lvl54_r2728
      lvl55_r2729
      lvl56_r272a
      lvl57_r272b
      lvl58_r272c
      lvl59_r272d
      lvl60_r272e
      lvl61_r272f
      lvl62_r272g
      lvl63_r272h
      lvl64_r272i
      lvl65_r272j
      lvl66_r272k
      lvl67_r272l
      lvl68_r272m
      lvl69_r272n
      lvl70_r272o
      lvl71_r272p
      lvl72_r272q
      $s$fApplicativeRWST_$c<*>_r272u
      $s$fApplicativeRWST_$cpure_r272v
      lvl74_r272w
      lvl75_r272x
      lvl76_r272y
      $s$fMonadRWST_$c>>_r272z
      $s$fMonadRWST_$cfail_r272A
      $s$fMonadRWST_$c>>=_r272B
      lvl77_r272C
      lvl78_r272D
      lvl79_r272E
      lvl80_r272F
      lvl81_r272G
      lvl82_r272H
      $slesser1_r272S
      lvl88_r272T
      lvl89_r272U
      $wcreate_r272V
      lvl90_r272W
      m2_r272X
      $s$fMonadReaderT_$c>>_r272Y
      $s$fMonadReaderT_$c>>=_r272Z
      go10_r2730
      $wpoly_create_r2731
      lvl91_r2732
      lvl92_r2733
      lvl93_r2734
      lvl94_r2735
      lvl95_r2736
      lvl96_r2737
      lvl97_r2738
      lvl98_r2739
      lvl99_r273a
      lvl100_r273b
      lvl101_r273c
      lvl102_r273d
      lvl103_r273e
      lvl104_r273f
      lvl105_r273g
      lvl106_r273h
      lvl107_r273i
      lvl108_r273j
      lvl109_r273k
      lvl110_r273l
      lvl111_r273m
      lvl112_r273n
      lvl113_r273o
      lvl114_r273p
      lvl115_r273q
      lvl116_r273r
      lvl117_r273s
      lvl118_r273t
      lvl119_r273u
      lvl120_r273v
      lvl121_r273w
      lvl122_r273x
      lvl123_r273y
      lvl124_r273z
      $wpoly_create1_r273A
      lvl125_r273B
      lvl126_r273C
      lvl127_r273D
      lvl128_r273E
      lvl129_r273F
      lvl130_r273G
      lvl131_r273H
      lvl132_r273I
      lvl133_r273J
      lvl134_r273K
      lvl135_r273L
      $wlvl_r273M
      lvl136_r273N
      $wlvl1_r273O
      lvl137_r273P
      $wlvl2_r273Q
      lvl138_r273R
      $wlvl3_r273S
      lvl139_r273T
      $wlvl4_r273U
      lvl140_r273V
      $wlvl5_r273W
      lvl141_r273X
      $wlvl6_r273Y
      lvl142_r273Z
      lvl143_r2740
      lvl144_r2741
      lvl145_r2742
      lvl146_r2743
      lvl147_r2744
      lvl148_r2745
      lvl149_r2746
      lvl150_r2747
      lvl151_r2748
      lvl152_r2749
      lvl153_r274a
      lvl154_r274b
      $s$fFunctorReaderT_$cfmap_r274c
      $s$fFunctorReaderT_$c<$_r274d
      lvl155_r274e
      lvl156_r274f
      $s$fApplicativeReaderT_$c<*>_r274g
      $s$fMonadReaderT_$creturn_r274h
      $s$fMonadReaderT_$cfail_r274i
      lvl157_r274j
      lvl158_r274k
      lvl159_r274l
      lvl160_r274m
      $d~_r274n
      lvl161_r274p
      lvl162_r274q
      lvl163_r274s
      lvl164_r274t
      lvl165_r274v
      lvl166_r274w
      lvl167_r274y
      lvl168_r274z
      lvl169_r274B
      lvl170_r274C
      lvl171_r274E
      lvl172_r274F
      lvl173_r274H
      lvl174_r274I
      lvl175_r274K
      lvl176_r274L
      lvl177_r274N
      lvl178_r274O
      lvl179_r274Q
      lvl180_r274R
      lvl181_r274T
      lvl182_r274U
      lvl183_r274V
      lvl184_r274W
      lvl185_r274X
      lvl186_r274Y
      lvl187_r274Z
      lvl188_r2750
      lvl189_r2751
      lvl190_r2752
      lvl191_r2753
      lvl192_r2754
      lvl193_r2755
      lvl194_r2756
      lvl195_r2757
      lvl196_r2758
      lvl197_r2759
      lvl198_r275a
      lvl199_r275b
      lvl200_r275c
      lvl201_r275d
      lvl202_r275e
      lvl203_r275f
      lvl204_r275g
      lvl205_r275h
      lvl206_r275i
      lvl207_r275j
      lvl208_r275k
      lvl209_r275l
      lvl210_r275m
      lvl211_r275n
      lvl212_r275o
      lvl213_r275p
      lvl214_r275q
      lvl215_r275r
      lvl216_r275s
      lvl217_r275t
      lvl218_r275u
      lvl219_r275v
      lvl220_r275w
      ww1_r275x
      ww2_r275y
      lvl221_r275z
      ww3_r275A
      lvl222_r275B
      pre_r275C
      x_s27MP
      eta_s27MQ
      eta1_s27MR
      ds_s27MS
      ds1_s27MT
      ds2_s27MU
      ds3_s27MV
      goal_s27MW
      prxy'_s27MX
      sat_s27MY
    
    Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Attachments (3)

Archive.zip (3.8 KB) - added by cipher1024 2 years ago.
Isolated example
Proofs2.hs (16.0 KB) - added by RyanGlScott 2 years ago.
Proofs2.core-lint (242.3 KB) - added by RyanGlScott 2 years ago.

Download all attachments as: .zip

Change History (38)

comment:1 Changed 2 years ago by cipher1024

Description: modified (diff)

comment:2 Changed 2 years ago by cipher1024

Description: modified (diff)

comment:3 Changed 2 years ago by mpickering

Status: newinfoneeded

What are you building?

comment:4 Changed 2 years ago by RyanGlScott

I suspect it's literate-unitb from here.

I was able to reproduce the panic, but literate-unitb is so complicated that I can't minimize the panic down to a single file with no dependencies. cipher1024, might you be able to trim the example down some so that we can help debug this further?

comment:5 Changed 2 years ago by RyanGlScott

Another useful check would be to build this with GHC HEAD. It's possible that this bug has already been fixed there (e.g., this might be a duplicate of #12944, but it's hard to tell).

comment:6 Changed 2 years ago by cipher1024

Good guess!

As for trimming it down, I'm not sure how to do it. How do you normally proceed? Is there a better approach to commenting out functions until I find one that breaks the compiler?

I'm going to try HEAD. If the fix exists, is there any chance it might get applied to ghc-8.0.1 and ghc-8.0.2?

comment:7 in reply to:  6 Changed 2 years ago by RyanGlScott

Replying to cipher1024:

How do you normally proceed? Is there a better approach to commenting out functions until I find one that breaks the compiler?

That's the approach I use, yes :)

I did recall that the issue appears when you trim down Document.Phase.Proofs to just liveness, stepList, and stepList' (you can replace some subexpressions, such as withCommand "\\safstep" $ safStep m, with undefined to help eliminate top-level definitions you don't need, like safStep). But after that point, the issue was tracking down all of the types imported from other modules and putting them all in one place. That's the point where I gave up, since trying to understand the innards of HasCell, Builder, LatexParserA, etc. proved too much for my feeble brain.

If the fix exists, is there any chance it might get applied to ghc-8.0.1 and ghc-8.0.2?

No. GHC 8.2.1 is going to be released soon, so if you help us discover a bug that still needs to be fixed, then it would get merged into 8.2.1 at the earliest.

comment:8 Changed 2 years ago by cipher1024

Yeah, the parser is fairly complex. Thank you for trying to minimize it yourself.

So here's a game plan:

  1. minimize the example
  2. get / build ghc HEAD
  3. try it on example.

I have never worked on ghc. What is the simplest way to get ghc HEAD to test my example with it?

comment:9 in reply to:  8 Changed 2 years ago by RyanGlScott

Replying to cipher1024:

What is the simplest way to get ghc HEAD to test my example with it?

If you're on Ubuntu, you can use this PPA to install ghc-8.2.1 or ghc-head (they're pretty much the same at this point) quite easily. Otherwise, you can use this link to get binary distributions of GHC 8.2.1-rc1 for Windows, OS X, or Linux.

comment:10 Changed 2 years ago by cipher1024

Awesome that helps a lot, thank you!

I departed from the plan just to see if ghc-8.2.1 has the bug still. Since most libraries don't support base-4.10.0.0 it didn't get far enough to tell. Is there is a way to disregard the libraries' upper bound on base? Could that work? Otherwise, I'll just get back to minimizing the example.

comment:11 in reply to:  10 Changed 2 years ago by RyanGlScott

Replying to cipher1024:

Is there is a way to disregard the libraries' upper bound on base? Could that work?

With cabal, that's possible with the --allow-newer flag. stack-1.4.0 and later apparently also has an allow-newer config option, although I've never tried that.

Changed 2 years ago by cipher1024

Attachment: Archive.zip added

Isolated example

comment:12 Changed 2 years ago by cipher1024

I just uploaded a restricted example. It is still 300 lines long. Is it helpful?

I'll keep working on it.

Changed 2 years ago by RyanGlScott

Attachment: Proofs2.hs added

comment:13 Changed 2 years ago by RyanGlScott

Thank you so much, cipher1024! That was tremendously helpful.

I've attached a version with no dependencies. Sadly, it gives the same panic on GHC 8.2.1 and HEAD. However, it does not panic on GHC 7.10.3–I'll see which commit caused this.

comment:14 Changed 2 years ago by RyanGlScott

Cc: simonmar added

Commit 8ecf6d8f7dfee9e5b1844cd196f83f00f3b6b879 (ApplicativeDo transformation) caused this regression.

comment:15 Changed 2 years ago by cipher1024

That's interesting. The LatexParser implements both Arrow and Applicative and I use the special Arrow notation. I wonder if the problem comes from the interplay between the arrow notation and the do notation.

comment:16 Changed 2 years ago by cipher1024

I find it a bit confusing because the commit dates back to 2015 while literate-unitb worked with ghc-8.0.1 up until november 2016. I don't know when it stopped working but nobody built it in the last couple of months.

comment:17 in reply to:  16 Changed 2 years ago by RyanGlScott

Replying to cipher1024:

I find it a bit confusing because the commit dates back to 2015 while literate-unitb worked with ghc-8.0.1 up until november 2016.

I'm not sure what you mean by this, especially since the version of Proofs2.hs that I attached also panics with GHC 8.0.1.

But moreover, it's important to note that you can't divide up GHC's commit history into discrete chunks corresponding to each GHC version. We operate by selectively merging commits from HEAD into release branches. So even though the ApplicativeDo patch was first committed back in 2015, it didn't actually appear in a major release (8.0) until much later, since we waited until we had made a couple of point releases for GHC 7.10 before putting new, breaking changes (including ApplicativeDo) in a major 8.0 release.

comment:18 Changed 2 years ago by cipher1024

Ok, I messed up. I was wrong. I thought it was building with ghc-8.0.1 but I think I was just using stack's lts-7 which normally uses ghc-8.0.1 but I didn't notice that I was specifying ghc-7.10.3. It's clearer now.

I was assuming that there might be different releases of ghc-8.0.1 but, after realizing my mistaking, I'm thinking you probably have a single commit corresponding to each release. Am I correct?

comment:19 in reply to:  18 Changed 2 years ago by RyanGlScott

Replying to cipher1024:

I was assuming that there might be different releases of ghc-8.0.1 but, after realizing my mistaking, I'm thinking you probably have a single commit corresponding to each release. Am I correct?

Correct. Once we make a release, it's frozen. For instance, here's the commit corresponding to the GHC 8.0.1 release: http://git.haskell.org/ghc.git/commit/4986837f8168cacf95c24fecc84d7b36c47f3c11

comment:20 Changed 2 years ago by simonpj

I bet -dcore-lint gives a much more helpful error message. Can you try that?

Simon

Changed 2 years ago by RyanGlScott

Attachment: Proofs2.core-lint added

comment:21 Changed 2 years ago by RyanGlScott

Sure thing. Here's the relevant bit of Core Lint error from the file I've attached:

[1 of 1] Compiling Document.Phase.Proofs2 ( Proofs2.hs, Proofs2.o )
*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: warning:
    In the expression: ds_d7Cx
                         @ (RawProgressProp, RuleProxy)
                         @ (RawProgressProp, Proxy a_a6xa)
                         @ VoidInference
                         (ds_d7Cx
                            @ (RawProgressProp, RuleProxy)
                            @ ((RuleProxy, ()), RawProgressProp)
                            @ (RawProgressProp, Proxy a_a6xa)
                            (ds_d7Cw
                               @ (RawProgressProp, RuleProxy)
                               @ ((RuleProxy, ()), RawProgressProp)
                               (\ (ds_d7CJ :: (RawProgressProp, RuleProxy)) ->
                                  case ds_d7CJ of { (goal_a58Y, prxy_a58Z) ->             
                                  ((prxy_a58Z, ()), goal_a58Y)                            
                                  }))                                                     
                            (ds_d7Cx                                                      
                               @ ((RuleProxy, ()), RawProgressProp)                       
                               @ (Cell1 Proxy RuleParser, RawProgressProp)                
                               @ (RawProgressProp, Proxy a_a6xa)                          
                               (first                                                     
                                  @ (LatexParserT M)
                                  $fArrowLatexParserT
                                  @ (RuleProxy, ())
                                  @ (Cell1 Proxy RuleParser)
                                  @ RawProgressProp
                                  (ds_d7Cx
                                     @ (RuleProxy, ())
                                     @ RuleProxy
                                     @ (Cell1 Proxy RuleParser)
                                     (ds_d7Cw
                                        @ (RuleProxy, ())
                                        @ RuleProxy
                                        (\ (ds_d7CH :: (RuleProxy, ())) ->
                                           case ds_d7CH of { (ds_d7CG, _ [Occ=Dead]) -> ds_d7CG }))
                                     (arr
                                        @ (LatexParserT M)
                                        $fArrowLatexParserT
                                        @ RuleProxy
                                        @ (Cell1 Proxy RuleParser)
                                        (view
                                           @ RuleProxy
                                           @ ((->) RuleProxy)
                                           @ (Cell1 Proxy RuleParser)
                                           ($fMonadReaderr(->) @ RuleProxy)
                                           (cell
                                              @ RuleProxy
                                              @ (Cell1 Proxy RuleParser)
                                              $fHasCellRuleProxyCell1
                                              @ (Const (Cell1 Proxy RuleParser))
                                              ($fFunctorConst @ (Cell1 Proxy RuleParser)))))))
                               (ds_d7Cw
                                  @ (Cell1 Proxy RuleParser, RawProgressProp)
                                  @ (RawProgressProp, Proxy a_a6xa)
                                  (\ (ds_d7CZ :: (Cell1 Proxy RuleParser, RawProgressProp)) ->
                                     case ds_d7CZ of { (ds_d7CM, ds_d7CK) ->
                                     case ds_d7CM of
                                     { Cell @ a_a6xa _ [Occ=Dead] _ [Occ=Dead] prxy'_a590 ->
                                     (ds_d7CK, prxy'_a590)
                                     }
                                     }))))
                         (ds_d7Cx
                            @ (RawProgressProp, Proxy a_a6xa)
                            @ ((RawProgressProp, Proxy a_a6xa), ())
                            @ VoidInference
                            (ds_d7Cw
                               @ (RawProgressProp, Proxy a_a6xa)
                               @ ((RawProgressProp, Proxy a_a6xa), ())
                               (\ (ds_d7CD :: (RawProgressProp, Proxy a_a6xa)) -> (ds_d7CD, ())))
                            (ds_d7Cx
                               @ ((RawProgressProp, Proxy a_a6xa), ())
                               @ (RawProgressProp, Inst1 Proxy RuleParser a_a6xa)
                               @ VoidInference
                               (ds_d7Cw
                                  @ ((RawProgressProp, Proxy a_a6xa), ())
                                  @ (RawProgressProp, Inst1 Proxy RuleParser a_a6xa)
                                  (\ (ds_d7CC :: ((RawProgressProp, Proxy a_a6xa), ())) ->
                                     case ds_d7CC of { (ds_d7CB, _ [Occ=Dead]) ->
                                     case ds_d7CB of { (goal_a58Y, prxy'_a590) ->
                                     (goal_a58Y,
                                      Inst
                                        @ Proxy
                                        @ RuleParser
                                        @ a_a6xa
                                        $dTypeable_a6xl
                                        irred_a6xm
                                        prxy'_a590)
                                     }
                                     }))
                               (stepList @ a_a6xa m_a58W)))
    @ a_a6xa is out of scope

comment:22 Changed 2 years ago by simonpj

Here is a much smaller test case. Still a big mess of applicative do and arrows, neither of which I am familiar with, alas.

{-# LANGUAGE Arrows #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

module Document.Phase.Proofs2 (step) where

import Control.Applicative
import Control.Arrow
import Control.Category

import Control.Monad
import Data.Functor.Compose
import Data.Maybe
import Data.Proxy
import Data.Typeable

import GHC.Exts (Constraint)

import Prelude hiding (id,(.))

data Inference rule
data MachineP3
data RawProgressProp

data Cell1 (f :: * -> *) (constr :: * -> Constraint)
   = forall a. (constr a, Typeable a) => Cell (f a)

data Inst1 f constr a = (Typeable a,constr a) => Inst (f a)

newtype RuleProxy = RuleProxy { _ruleProxyCell :: Cell1 Proxy RuleParser }


type VoidInference = Cell1 (Compose Inference Proxy) RuleParser

class Monad m => MonadReader r m | m -> r where

instance MonadReader r ((->) r) where

class RuleParser rule where

type Lens' s a = Lens s s a a
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
type Getting r s a = (a -> Const r a) -> s -> Const r s

class HasCell s a | s -> a where

instance HasCell RuleProxy (Cell1 (Proxy :: * -> *) RuleParser) where

data LatexParserA a g = LatexParserA
instance Category LatexParserA where
instance Arrow    LatexParserA  where


-----------------------------
stepList :: MachineP3
         -> LatexParserA (RawProgressProp,Inst1 Proxy RuleParser rule) VoidInference
stepList m = error "urk"

step :: MachineP3 -> LatexParserA (RawProgressProp,RuleProxy) VoidInference
step m = insideOneEnvOf ["step","flatstep"] $ proc (goal,prxy) -> do
                Cell prxy' <- arr (view xcell) -< prxy
                stepList m -< (goal,Inst prxy')

view :: MonadReader s m => Getting a s a -> m a
view l = error "urk"

insideOneEnvOf :: [String] -> LatexParserA a b -> LatexParserA a b
insideOneEnvOf = error "urk"


xcell :: HasCell s a => Lens' s a
xcell = error "urk"

comment:23 Changed 2 years ago by simonpj

Keywords: ApplicativeDo Arrows added

comment:24 Changed 2 years ago by simonpj

Keywords: ApplicativeDo removed

Actually, it's nothing to do with applicative-do (that extension is not used).

Is anyone familiar with arrows who can debug this?

It fails with GHC 7.10 as well, so I'm not sure it ever worked...

Maybe someone can cut it down still further...

comment:25 Changed 2 years ago by simonpj

Status: infoneedednew

comment:26 Changed 2 years ago by simonpj

Summary: ghc: panic! StgCmmEnv: variable not foundLint error in arrows program

comment:27 in reply to:  24 Changed 2 years ago by RyanGlScott

Replying to simonpj:

It fails with GHC 7.10 as well, so I'm not sure it ever worked...

What do you mean? It works fine with GHC 7.10.3:

$ /opt/ghc/7.10.3/bin/ghc Bug.hs -fforce-recomp
[1 of 1] Compiling Document.Phase.Proofs2 ( Bug.hs, Bug.o )

Bug.hs:60:10: Warning:
    No explicit implementation for
      ‘id’ and ‘.’
    In the instance declaration for ‘Category LatexParserA’

Bug.hs:61:10: Warning:
    No explicit implementation for
      ‘arr’ and ‘first’
    In the instance declaration for ‘Arrow LatexParserA’

Aside from some warnings, of course, which are due to minimizing the program down so much.

comment:28 Changed 2 years ago by cipher1024

Aside from some warnings, of course, which are due to minimizing the program down so much.

With ghc-7.10.3, compiling with -dcore-lint I get a similar Core Lint errors.

I have trimmed down the example further (see below). It seems to be a product of the interplay between existential types and arrow notation.

The problem seems to come up because an existential type variable becomes free as a result of the following statement:

Cell prxy' <- id -< prxy

After staring at it for a minute or so, I find that I cannot desugar the arrow notation in step. The obvious candidate is:

step = id >>> arr (\(Cell prxy) -> prxy) >>> stepList

but the internal function (\(Cell prxy) -> prxy) cannot be given a type because of the existential type of Cell. Could this be related to the bug?


{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Arrows #-}
module Document.Phase.Proofs2 (step) where

import Control.Arrow
import Control.Category

import Data.Proxy

import Prelude hiding (id,(.))

data Cell1
   = forall a. Cell (Proxy a)

data LatexParserA a g = LatexParserA
instance Category LatexParserA where
instance Arrow    LatexParserA  where

-----------------------------

stepList :: LatexParserA (Proxy rule) r
stepList = error "urk"

step :: LatexParserA Cell1 r
step = proc prxy -> do
                Cell prxy' <- id -< prxy
                stepList -< prxy'

comment:29 Changed 2 years ago by simonpj

Cc: Henrik.Nilsson@… Ross Paterson <ross@…> added; simonmar removed

Thanks for boiling it down so much futher.

I have only the vaguest idea about how arrow-desugaring works, but I think it's very likely that it won't work at all if there are existentials involved. Would an arrow expert care to give an opinion? Henrik? Ross?

If so, we should reject it in a civilised way, not crash.

Generally, arrows are sorely in need of love.

comment:30 Changed 2 years ago by cipher1024

What kind of attention do you think Arrows need? I haven't contributed to GHC before but if I can help with arrows I'd love to.

In this particular situation, beside needing a more civilized error message, maybe we need a generalization of ArrowChoice for existential types so that we can make this design work:

class Arrow arr => ArrowExist arr where
    existentially :: (forall a. constr a => arr (f a) b) -> arr (Cell1 f constr) b

with

data Cell1 f (constr :: * -> Constraint) = forall a. (constr a, Typeable a) => Cell (f a)
   -- from https://hackage.haskell.org/package/existential

It might be overkill though. Looking back, maybe I'm overusing existential types.

comment:31 Changed 2 years ago by RyanGlScott

cipher1024, is my understanding of arrows correct in that the arrow notation you use in step would desugar down to something like this?

step :: LatexParserA Cell1 r
step = arr (\prxy -> prxy) >>> id >>> arr (\(Cell prxy') -> prxy') >>> stepList

If so, the Core Lint error is somewhat understandable, as trying to typecheck that code simply won't work:

Bug.hs:25:61: error:
    • Couldn't match type ‘rule0’ with ‘a’
        because type variable ‘a’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a pattern with constructor: Cell :: forall a. Proxy a -> Cell1,
        in a lambda abstraction
        at Bug.hs:25:46-55
      Expected type: Proxy rule0
        Actual type: Proxy a
    • In the expression: prxy'
      In the first argument of ‘arr’, namely ‘(\ (Cell prxy') -> prxy')’
      In the first argument of ‘(>>>)’, namely
        ‘arr (\ (Cell prxy') -> prxy')’
    • Relevant bindings include
        prxy' :: Proxy a (bound at Bug.hs:25:51)

comment:32 Changed 2 years ago by simonpj

What kind of attention do you think Arrows need? I haven't contributed to GHC before but if I can help with arrows I'd love to

Great! Check out ArrowNotation!

comment:33 Changed 2 years ago by simonpj

If so, the Core Lint error is somewhat understandable

Yes, but if existentials are not valid in arrow notation, the typechecker should reject the program cleanly, rather than producing invalid Core.

comment:34 Changed 2 years ago by RyanGlScott

comment:35 Changed 16 months ago by RyanGlScott

Note: See TracTickets for help on using tickets.