nick8325 / quickspec

Equational laws for free
BSD 3-Clause "New" or "Revised" License
250 stars 24 forks source link

Why is quickspec introducing type variables in monomorphic code? #41

Open isovector opened 4 years ago

isovector commented 4 years ago

My sig:

== Functions ==                  
   subst1 :: Subst1 -> LexemeVW' () () -> [LexemeVW' () ()]
      var :: Var -> LexemeVW' () ()
      lex :: Lexeme -> LexemeVW' () ()
    white :: Whitespace -> LexemeVW' () ()
  mkSubst :: Var -> [LexemeVW' Void ()] -> Subst1
     both :: [LexemeVW' Void ()] -> [LexemeVW' Void ()] -> [LexemeVW' Void ()]
    bothP :: [LexemeVW' () ()] -> [LexemeVW' () ()] -> [LexemeVW' () ()]
   emptyP :: [LexemeVW' () ()]
toPattern :: LexemeVW' () () -> [LexemeVW' () ()]
 toSource :: LexemeVW' Void () -> [LexemeVW' Void ()]

WARNING: The following types have no 'Arbitrary' instance declared.
You will not get any variables of the following types:
  LexemeVW' Int Int
  LexemeVW' Int ()
  LexemeVW' () Int
  LexemeVW' Void Int
  [LexemeVW' Int Int]
  [LexemeVW' Int ()]
  [LexemeVW' () Int]
  [LexemeVW' Void Int]

Where do these warnings come from? Absolutely everything in the signature is monomporphic, so it shouldn't be defaulting to Int, should it?

nick8325 commented 4 years ago

Right, this warning is spurious. QuickSpec computes the set of all types that might occur in a generated term. This information is used internally and so it's important that every type that might be needed actually occurs in this set. For this reason QuickSpec computes a (quite crude) overapproximation of the set of types, which in this case includes the rather silly examples you saw.

Computing the set of types accurately is a little bit tricky: variables have the polymorphic type 'a' so there is always at least one polymorphic type, and two terms that have unifiable types will be instantiated at their most general unifier so it's not enough to look at single terms in isolation. But it makes sense to spend the extra effort to compute the set of types accurately.

isovector commented 4 years ago

This has become very painful when working with polymorphic types. Here's some QuickSpec output I got today:

You will not get any variables of the following types:                                            
  MultiSet Int                                                                                    
  InputFilter Int                                                                                 
  InputFilter (MultiSet Int)                                                                      
  InputFilter (MultiSet RewardContents)                                                           
  Challenge Int Int Int                                                                           
  Challenge Int Int Scavenge                                                                      
  Challenge Int Scavenge Int                                                                      
  Challenge Scavenge Int Int                                                                      
  Challenge Int Int [Int]                                                                         
  Challenge Int Int [Bool]                                                                        
  Challenge Int Int (MultiSet Int)                                                                
  Challenge Int Int (MultiSet RewardContents)                                                     
  Challenge Int Scavenge [Int]                                                                    
  Challenge Int Scavenge [Bool]                                                                   
  Challenge Int Scavenge (MultiSet Int)                                                           
  Challenge Int Scavenge (MultiSet RewardContents)                                                
  Challenge Int [Int] Int                                                                         
  Challenge Int [Int] Scavenge                                                                    
  Challenge Int [Bool] Int                                                                        
  Challenge Int [Bool] Scavenge                                                                   
  Challenge Scavenge Int (MultiSet Int)                                                           
  Challenge Scavenge Int (MultiSet RewardContents)                                                
  Challenge Scavenge [Int] Int                                                                    
  Challenge Scavenge [Bool] Int                                                                   
  Challenge [Int] Int Int                                                                         
  Challenge [Int] Scavenge Int                                                                    
  Challenge [Bool] Int Int                                                                        
  Challenge [Bool] Scavenge Int                                                                   
  Challenge (MultiSet Int) Int Int                                                                
  Challenge (MultiSet Int) Int Scavenge                                                           
  Challenge (MultiSet Int) Scavenge Int                                                           
  Challenge (MultiSet RewardContents) Int Int                                                     
  Challenge (MultiSet RewardContents) Int Scavenge                                                
  Challenge (MultiSet RewardContents) Scavenge Int                                                
  Challenge Int [Int] (MultiSet Int)                                                              
  Challenge Int [Int] (MultiSet RewardContents)                                                   
  Challenge Int [Bool] (MultiSet Int)                                                             
  Challenge Int [Bool] (MultiSet RewardContents)                                                  
  Challenge Scavenge [Int] (MultiSet Int)                                                         
  Challenge Scavenge [Int] (MultiSet RewardContents)                                              
  Challenge Scavenge [Bool] (MultiSet Int)                                                        
  Challenge [Int] Int (MultiSet Int)                                                              
  Challenge [Int] Int (MultiSet RewardContents)                                                   
  Challenge [Int] Scavenge (MultiSet Int)                                                         
  Challenge [Int] Scavenge (MultiSet RewardContents)                                              
  Challenge [Bool] Int (MultiSet Int)                                                             
  Challenge [Bool] Int (MultiSet RewardContents)                                                  
  Challenge [Bool] Scavenge (MultiSet Int)                                                        
  Challenge [Bool] Scavenge (MultiSet RewardContents)                                             
  Challenge (MultiSet Int) Int [Int]                                                              
  Challenge (MultiSet Int) Int [Bool]                                                             
  Challenge (MultiSet Int) Scavenge [Int]                                                         
  Challenge (MultiSet Int) Scavenge [Bool]                                                        
  Challenge (MultiSet Int) [Int] Int                                                              
  Challenge (MultiSet Int) [Int] Scavenge                                                         
  Challenge (MultiSet Int) [Bool] Int
  Challenge (MultiSet Int) [Bool] Scavenge
  Challenge (MultiSet RewardContents) Int [Int]
  Challenge (MultiSet RewardContents) Int [Bool]
  Challenge (MultiSet RewardContents) Scavenge [Int]

You will not get any equations about the following types:                                [15/2643]
  MultiSet Int                                                                                    
  InputFilter Int                                                                                 
  InputFilter (MultiSet Int)                                                                      
  InputFilter (MultiSet RewardContents)                                                           
  Challenge Int Int Int                                                                           
  Challenge Int Int Scavenge                                                                      
  Challenge Int Scavenge Int                                                                      
  Challenge Scavenge Int Int                                                                      
  Challenge Int Int [Int]                                                                         
  Challenge Int Int [Bool]                                                                        
  Challenge Int Int (MultiSet Int)                                                                
  Challenge Int Int (MultiSet RewardContents)                                                     
  Challenge Int Scavenge [Int]                                                                    
  Challenge Int Scavenge [Bool]                                                                   
  Challenge Int Scavenge (MultiSet Int)                                                           
  Challenge Int Scavenge (MultiSet RewardContents)
  Challenge Int [Int] Int
  Challenge Int [Int] Scavenge
  Challenge Int [Bool] Int
  Challenge Int [Bool] Scavenge
  Challenge Scavenge Int (MultiSet Int)
  Challenge Scavenge Int (MultiSet RewardContents)
  Challenge Scavenge [Int] Int
  Challenge Scavenge [Bool] Int
  Challenge [Int] Int Int
  Challenge [Int] Scavenge Int
  Challenge [Bool] Int Int
  Challenge [Bool] Scavenge Int
  Challenge (MultiSet Int) Int Int
  Challenge (MultiSet Int) Int Scavenge
  Challenge (MultiSet Int) Scavenge Int
  Challenge (MultiSet RewardContents) Int Int
  Challenge (MultiSet RewardContents) Int Scavenge
  Challenge (MultiSet RewardContents) Scavenge Int
  Challenge Int [Int] (MultiSet Int)
  Challenge Int [Int] (MultiSet RewardContents)
  Challenge Int [Bool] (MultiSet Int)
  Challenge Int [Bool] (MultiSet RewardContents)
  Challenge Scavenge [Int] (MultiSet Int)
  Challenge Scavenge [Int] (MultiSet RewardContents)
  Challenge Scavenge [Bool] (MultiSet Int)
  Challenge [Int] Int (MultiSet Int)
  Challenge [Int] Int (MultiSet RewardContents)
  Challenge [Int] Scavenge (MultiSet Int)
  Challenge [Int] Scavenge (MultiSet RewardContents)
  Challenge [Bool] Int (MultiSet Int)
  Challenge [Bool] Int (MultiSet RewardContents)
  Challenge [Bool] Scavenge (MultiSet Int)
  Challenge [Bool] Scavenge (MultiSet RewardContents)
  Challenge (MultiSet Int) Int [Int]
  Challenge (MultiSet Int) Int [Bool]
  Challenge (MultiSet Int) Scavenge [Int]
  Challenge (MultiSet Int) Scavenge [Bool]
  Challenge (MultiSet Int) [Int] Int
  Challenge (MultiSet Int) [Int] Scavenge
  Challenge (MultiSet Int) [Bool] Int
  Challenge (MultiSet Int) [Bool] Scavenge
  Challenge (MultiSet RewardContents) Int [Int]
  Challenge (MultiSet RewardContents) Int [Bool]
  Challenge (MultiSet RewardContents) Scavenge [Int]
  Challenge (MultiSet RewardContents) Scavenge [Bool]

There's so much noise here that I have no idea if there are genuine warnings.

isovector commented 4 years ago

the signature:

   both :: Challenge Scavenge [Bool] (MultiSet RewardContents) -> Challenge Scavenge [Bool] (Multi
Set RewardContents) -> Challenge Scavenge [Bool] (MultiSet RewardContents)                        
eitherC :: Challenge Scavenge [Bool] (MultiSet RewardContents) -> Challenge Scavenge [Bool] (Multi
Set RewardContents) -> Challenge Scavenge [Bool] (MultiSet RewardContents)                        
  empty :: Challenge (MultiSet RewardContents) Scavenge [Bool]                                    
andThen :: Challenge Scavenge [Bool] (MultiSet RewardContents) -> Challenge Scavenge [Bool] (Multi
Set RewardContents) -> Challenge Scavenge [Bool] (MultiSet RewardContents)                        
 reward :: MultiSet RewardContents -> Challenge [Bool] Scavenge (MultiSet RewardContents)         
 pruned :: Challenge [Bool] Scavenge (MultiSet RewardContents) -> Challenge [Bool] Scavenge (Multi
Set RewardContents)                                                                               
   gate :: InputFilter (MultiSet RewardContents) -> Challenge (MultiSet RewardContents) [Bool] Sca
venge -> Challenge (MultiSet RewardContents) [Bool] Scavenge                                      
 always :: InputFilter Scavenge                                                                   
  never :: InputFilter Scavenge                                                                   
 mempty :: Monoid a => a                                                                          
   (<>) :: Monoid a => a -> a -> a