Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,393
    • Issues 4,393
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 381
    • Merge Requests 381
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #19324

Closed
Open
Opened Feb 04, 2021 by Andrzej Rybczak@arybczakContributor

unsafeEqualityProof shows in generated core

Several tests from optics that use inspection-testing fail with GHC 9.0.1 because of this, e.g.

        tests/Optics/Tests/Utils.hs:56:
        tests/Optics/Tests/Labels/TH.hs:61:20: label5lhs ==- label5rhs failed:            
            LHS:                                                                          
                label5lhs = label5lhs_szze `cast` <Co:31>                                 
                                                                                          
                label5lhs_szze                                                            
                  = \ @a @b s name_ age_ fishName_ pets_ ->                               
                      case unsafeEqualityProof of { UnsafeRefl co2 ->
                      case s of { Human x1_af3x x2_af3y x3_af3z x4_af3A ->
                      (Human
                         name_
                         age_
                         (case x3_af3z of {
                            GoldFish x1_aeS2 -> GoldFish fishName_;
                            Herring x1_aeS4 -> Herring fishName_
                          })
                         pets_)
                      `cast` <Co:4>
                      }
                      }
                
            RHS:
                label5rhs
                  = \ @a @b s name_ age_ fishName_ pets_ ->
                      case s of { Human ds_dpF7 ds_dpF8 ds_dpF9 ds_dpFa ->
                      Human
                        name_
                        age_
                        (case ds_dpF9 of {
                           GoldFish ds_dpEY -> GoldFish fishName_;
                           Herring ds_dpEZ -> Herring fishName_
                         })
                        pets_
                      }
Core without -dsuppress-all
        tests/Optics/Tests/Utils.hs:56:
        tests/Optics/Tests/Labels/TH.hs:61:20: label5lhs ==- label5rhs failed:                                                                                                                                                                                                                                                                                                                                                                
            LHS:                                                                                                                                                                                                                                                                                                                                                                                                                              
                label5lhs                                                                                                                                                                                                                                                                                                                                                                                                                     
                  :: forall a b. Human a -> String -> Int -> String -> [b] -> Human b                                                                                                                                                                                                                                                                                                                                                         
                [LclIdX,                                                                                                                                                                                                                                                                                                                                                                                                                      
                 Arity=5,                                                                                                                                                                                                                                                                                                                                                                                                                     
                 Str=<S,1*U(A,A,1*U,A)><L,U><L,U><L,U><L,U>,                                                                                                                                                                                                                                                                                                                                                                                  
                 Cpr=m1,                                                                                                                                                                                                                                                                                                                                                                                                                      
                 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,                                                                                                                                                                                                                                                                                                                                                             
                         WorkFree=True, Expandable=True,                                                                                                                                                                                                                                                                                                                                                                                      
                         Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)                                                                                                                                                                                                                                                                                                                                                             
                         Tmpl= label5lhs_sf4S                                                                                                                                                                                                                                                                                                                                                                                                 
                               `cast` (forall (a :: <*>_N) (b :: <*>_N).                                                                                                                                                                                                                                                                                                                                                                      
                                       <Human a>_R                                                                                                                                                                                                                                                                                                                                                                                            
                                       %<'Many>_N ->_R <String>_R                                                                                                                                                                                                                                                                                                                                                                             
                                       %<'Many>_N ->_R <Int>_R                                                                                                                                                                                                                                                                                                                                                                                
                                       %<'Many>_N ->_R <String>_R                                                                                                                                                                                                                                                                                                                                                                             
                                       %<'Many>_N ->_R <[b]>_R                                                                                                                                                                                                                                                                                                                                                                                
                                       %<'Many>_N ->_R Nth:4                                                                                                                                                                                                                                                                                                                                                                                  
                                                           (<Human a>_R                                                                                                                                                                                                                                                                                                                                                                       
                                                            %<'Many>_N ->_R N:Identity[0] <Human b>_R)                                                                                                                                                                                                                                                                                                                                        
                                       :: Coercible                                                                                                                                                                                                                                                                                                                                                                                           
                                            (forall {a} {b}.                                                                                                                                                                                                                                                                                                                                                                                  
                                             Human a                                                                                                                                                                                                                                                                                                                                                                                          
                                             -> String -> Int -> String -> [b] -> Identity (Human b))                                                                                                                                                                                                                                                                                                                                         
                                            (forall {a} {b}.                                                                                                                                                                                                                                                                                                                                                                                  
                                             Human a -> String -> Int -> String -> [b] -> Human b))}]                                                                                                                                                                                                                                                                                                                                         
                label5lhs                                                                                                                                                                                                                                                                                                                                                                                                                     
                  = label5lhs_sf4S                                                                                                                                                                                                                                                                                                                                                                                                            
                    `cast` (forall (a :: <*>_N) (b :: <*>_N).                                                                                                                                                                                                                                                                                                                                                                                 
                            <Human a>_R                                                                                                                                                                                                                                                                                                                                                                                                       
                            %<'Many>_N ->_R <String>_R                                                                                                                                                                                                                                                                                                                                                                                        
                            %<'Many>_N ->_R <Int>_R                                                                                                                                                                                                                                                                                                                                                                                           
                            %<'Many>_N ->_R <String>_R                                                                                                                                                                                                                                                                                                                                                                                        
                            %<'Many>_N ->_R <[b]>_R                                                                                                                                                                                                                                                                                                                                                                                           
                            %<'Many>_N ->_R Nth:4                                                                                                                                                                                                                                                                                                                                                                                             
                                                (<Human a>_R %<'Many>_N ->_R N:Identity[0] <Human b>_R)                                                                                                                                                                                                                                                                                                                                       
                            :: Coercible                                                                                                                                                                                                                                                                                                                                                                                                      
                                 (forall {a} {b}.                                                                                                                                                                                                                                                                                                                                                                                             
                                  Human a -> String -> Int -> String -> [b] -> Identity (Human b))                                                                                                                                                                                                                                                                                                                                            
                                 (forall {a} {b}.                                                                                                                                                                                                                                                                                                                                                                                             
                                  Human a -> String -> Int -> String -> [b] -> Human b))                                                                                                                                                                                                                                                                                                                                                      
                                                                                                                                                                                                                                                                                                                                                                                                                                              
                label5lhs_sf4S                                                                                                                                                                                                                                                                                                                                                                                                                
                  :: forall {a} {b}.                                                                                                                                                                                                                                                                                                                                                                                                          
                     Human a -> String -> Int -> String -> [b] -> Identity (Human b)                                                                                                                                                                                                                                                                                                                                                          
                [LclId,                                                                                                                                                                                                                                                                                                                                                                                                                       
                 Arity=5,                                                                                                                                                                                                                                                                                                                                                                                                                     
                 Str=<S,1*U(A,A,1*U,A)><L,U><L,U><L,U><L,U>,                                                                                                                                                                                                                                                                                                                                                                                  
                 Cpr=m1,                                                                                                                                                                                                                                                                                                                                                                                                                      
                 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,                                                                                                                                                                                                                                                                                                                                                             
                         WorkFree=True, Expandable=True,                                                                                                                                                                                                                                                                                                                                                                                      
                         Guidance=ALWAYS_IF(arity=5,unsat_ok=True,boring_ok=False)                                                                                                                                                                                                                                                                                                                                                            
                         Tmpl= \ (@a)                                                                                                                                                                                                                                                                                                                                                                                                         
                                 (@b)                                                                                                                                                                                                                                                                                                                                                                                                         
                                 (s [Occ=Once1!] :: Human a)                                                                                                                                                                                                                                                                                                                                                                                  
                                 (name_ [Occ=Once1] :: String)                                                                                                                                                                                                                                                                                                                                                                                
                                 (age_ [Occ=Once1] :: Int)                                                                                                                                                                                                                                                                                                                                                                                    
                                 (fishName_ [Occ=Once2] :: String)                                                                                                                                                                                                                                                                                                                                                                            
                                 (pets_ [Occ=Once1] :: [b]) ->                                                                                                                                                                                                                                                                                                                                                                                
                                 case unsafeEqualityProof                                                                                                                                                                                                                                                                                                                                                                                     
                                        @(*)                                                                                                                                                                                                                                                                                                                                                                                                  
                                        @(Any :~: Any)                                                                                                                                                                                                                                                                                                                                                                                        
                                        @(Curry NoIx (Curry NoIx Any) :~: Curry (Append NoIx NoIx) Any)                                                                                                                                                                                                                                                                                                                                       
                                 of                                                                                                                                                                                                                                                                                                                                                                                                           
                                 { UnsafeRefl co2 ->                                                                                                                                                                                                                                                                                                                                                                                          
                                 case s of                                                                                                                                                                                                                                                                                                                                                                                                    
                                 { Human _ [Occ=Dead] _ [Occ=Dead] x3_aaiE [Occ=Once1!]                                                                                                                                                                                                                                                                                                                                                       
                                         _ [Occ=Dead] ->                                                                                                                                                                                                                                                                                                                                                                                      
                                 (Human                                                                                                                                                                                                                                                                                                                                                                                                       
                                    @b                                                                                                                                                                                                                                                                                                                                                                                                        
                                    name_                                                                                                                                                                                                                                                                                                                                                                                                     
                                    age_                                                                                                                                                                                                                                                                                                                                                                                                      
                                    (case x3_aaiE of {                                                                                                                                                                                                                                                                                                                                                                                        
                                       GoldFish _ [Occ=Dead] -> GoldFish fishName_;                                                                                                                                                                                                                                                                                                                                                           
                                       Herring _ [Occ=Dead] -> Herring fishName_                                                                                                                                                                                                                                                                                                                                                              
                                     })                                                                                                                                                                                                                                                                                                                                                                                                       
                                    pets_)                                                                                                                                                                                                                                                                                                                                                                                                    
                                 `cast` (Sym (N:Identity[0] <Human b>_R)                                                                                                                                                                                                                                                                                                                                                                      
                                         :: Coercible (Human b) (Identity (Human b)))                                                                                                                                                                                                                                                                                                                                                         
                                 }                                                                                                                                                                                                                                                                                                                                                                                                            
                                 }}]                                                                                                                                                                                                                                                                                                                                                                                                          
                label5lhs_sf4S                                                                                                                                                                                                                                                                                                                                                                                                                
                  = \ (@a)                                                                                                                                                                                                                                                                                                                                                                                                                    
                      (@b)                                                                                                                                                                                                                                                                                                                                                                                                                    
                      (s [Dmd=<S,1*U(A,A,1*U,A)>] :: Human a)                                                                                                                                                                                                                                                                                                                                                                                 
                      (name_ :: String)                                                                                                                                                                                                                                                                                                                                                                                                       
                      (age_ :: Int)                                                                                                                                                                                                                                                                                                                                                                                                           
                      (fishName_ :: String)                                                                                                                                                                                                                                                                                                                                                                                                   
                      (pets_ :: [b]) ->                                                                                                                                                                                                                                                                                                                                                                                                       
                      case unsafeEqualityProof                                                                                                                                                                                                                                                                                                                                                                                                
                             @(*)                                                                                                                                                                                                                                                                                                                                                                                                             
                             @(Any :~: Any)                                                                                                                                                                                                                                                                                                                                                                                                   
                             @(Curry NoIx (Curry NoIx Any) :~: Curry (Append NoIx NoIx) Any)                                                                                                                                                                                                                                                                                                                                                  
                      of                                                                                                                                                                                                                                                                                                                                                                                                                      
                      { UnsafeRefl co2 [Dmd=<L,A>] ->                                                                                                                                                                                                                                                                                                                                                                                         
                      case s of                                                                                                                                                                                                                                                                                                                                                                                                               
                      { Human x1_aaiC [Dmd=<L,A>] x2_aaiD [Dmd=<L,A>]                                                                                                                                                                                                                                                                                                                                                                         
                              x3_aaiE [Dmd=<L,1*U>] x4_aaiF [Dmd=<L,A>] ->                                                                                                                                                                                                                                                                                                                                                                    
                      (Human                                                                                                                                                                                                                                                                                                                                                                                                                  
                         @b                                                                                                                                                                                                                                                                                                                                                                                                                   
                         name_                                                                                                                                                                                                                                                                                                                                                                                                                
                         age_                                                                                                                                                                                                                                                                                                                                                                                                                 
                         (case x3_aaiE of {                                                                                                                                                                                                                                                                                                                                                                                                   
                            GoldFish x1_aadU [Dmd=<L,A>] -> GoldFish fishName_;                                                                                                                                                                                                                                                                                                                                                               
                            Herring x1_aadW [Dmd=<L,A>] -> Herring fishName_                                                                                                                                                                                                                                                                                                                                                                  
                          })                                                                                                                                                                                                                                                                                                                                                                                                                  
                         pets_)                                                                                                                                                                                                                                                                                                                                                                                                               
                      `cast` (Sym (N:Identity[0] <Human b>_R)                                                                                                                                                                                                                                                                                                                                                                                 
                              :: Coercible (Human b) (Identity (Human b)))                                                                                                                                                                                                                                                                                                                                                                    
                      }                                                                                                                                                                                                                                                                                                                                                                                                                       
                      }                                                                                                                                                                                                                                                                                                                                                                                                                       
                                                                                                                                                                                                                                                                                                                                                                                                                                              
            RHS:                                                                                                                                                                                                                                                                                                                                                                                                                              
                label5rhs                                                                                                                                                                                                                                                                                                                                                                                                                     
                  :: forall a b. Human a -> String -> Int -> String -> [b] -> Human b                                                                                                                                                                                                                                                                                                                                                         
                [LclIdX,                                                                                                                                                                                                                                                                                                                                                                                                                      
                 Arity=5,                                                                                                                                                                                                                                                                                                                                                                                                                     
                 Str=<S,1*U(A,A,1*U,A)><L,U><L,U><L,U><L,U>,                                                                                                                                                                                                                                                                                                                                                                                  
                 Cpr=m1,                                                                                                                                                                                                                                                                                                                                                                                                                      
                 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,                                                                                                                                                                                                                                                                                                                                                             
                         WorkFree=True, Expandable=True,                                                                                                                                                                                                                                                                                                                                                                                      
                         Guidance=ALWAYS_IF(arity=5,unsat_ok=True,boring_ok=True)                                                                                                                                                                                                                                                                                                                                                             
                         Tmpl= \ (@a)                                                                                                                                                                                                                                                                                                                                                                                                         
                                 (@b)                                                                                                                                                                                                                                                                                                                                                                                                         
                                 (s [Occ=Once1!] :: Human a)                                                                                                                                                                                                                                                                                                                                                                                  
                                 (name_ [Occ=Once1] :: String)                                                                                                                                                                                                                                                                                                                                                                                
                                 (age_ [Occ=Once1] :: Int)                                                                                                                                                                                                                                                                                                                                                                                    
                                 (fishName_ [Occ=Once2] :: String)                                                                                                                                                                                                                                                                                                                                                                            
                                 (pets_ [Occ=Once1] :: [b]) ->                                                                                                                                                                                                                                                                                                                                                                                
                                 case s of                                                                                                                                                                                                                                                                                                                                                                                                    
                                 { Human _ [Occ=Dead] _ [Occ=Dead] ds_delQ [Occ=Once1!]                                                                                                                                                                                                                                                                                                                                                       
                                         _ [Occ=Dead] ->                                                                                                                                                                                                                                                                                                                                                                                      
                                 Human                                                                                                                                                                                                                                                                                                                                                                                                        
                                   @b                                                                                                                                                                                                                                                                                                                                                                                                         
                                   name_
                                   age_
                                   (case ds_delQ of {
                                      GoldFish _ [Occ=Dead] -> GoldFish fishName_;
                                      Herring _ [Occ=Dead] -> Herring fishName_
                                    })
                                   pets_
                                 }}]
                label5rhs
                  = \ (@a)
                      (@b)
                      (s [Dmd=<S,1*U(A,A,1*U,A)>] :: Human a)
                      (name_ :: String)
                      (age_ :: Int)
                      (fishName_ :: String)
                      (pets_ :: [b]) ->
                      case s of
                      { Human ds_delO [Dmd=<L,A>] ds_delP [Dmd=<L,A>]
                              ds_delQ [Dmd=<L,1*U>] ds_delR [Dmd=<L,A>] ->
                      Human
                        @b
                        name_
                        age_
                        (case ds_delQ of {
                           GoldFish ds_delF [Dmd=<L,A>] -> GoldFish fishName_;
                           Herring ds_delG [Dmd=<L,A>] -> Herring fishName_
                         })
                        pets_
                      }

These didn't show up in GHC <= 8.10. IIRC I've seen them in the past in GHC compiled from git, but never in a release. Is that change intentional?

Edited Feb 04, 2021 by Andrzej Rybczak
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#19324