Unable to understand coding logic / principle / convention - why 'Show a' is needed? Why 'Show Car" or "Show String" is not working?

Question

Code given below compiles, ok.

data Car p q r = Car {company :: p  
                     , model :: q  
                     , year ::r  
                     } deriving (Show)


tellCar :: (Show a) => Car String String a -> String

What are the basic principles/ conventions / logic which can remind me that I need to take 'Show a' only in 'tellCar', not any other option? Where can I find resource to learn such principles/ conventions / logic?

If I mistakenly take 'Show Car' in the tellCar, following error message is received on compilation:

*Main> :load "/home/optimight/baby.hs"  
[1 of 1] Compiling Main             ( /home/optimight/baby.hs, interpreted )  

/home/optimight/baby.hs:96:18:  
    Expecting three more arguments to `Car'  
    In the type signature for `tellCar':  
      tellCar :: Show Car => Car String String a -> String  
Failed, modules loaded: none.  

If I mistakenly take 'Show z' in the tellCar, following error message is received on compilation:

*Main> :load "/home/optimight/baby.hs"  
[1 of 1] Compiling Main               ( /home/optimight/baby.hs, interpreted )

/home/optimight/baby.hs:96:1:  
    Ambiguous constraint `Show z'  
      At least one of the forall'd type variables mentioned by the constraint  
      must be reachable from the type after the '=>'  
    In the type signature for `tellCar':  
      tellCar :: Show z => Car String String a -> String  
Failed, modules loaded: none.   

If I mistakenly take 'Show String' in the tellCar, following error message is received on compilation:

Prelude> :load "/home/optimight/baby.hs"  
[1 of 1] Compiling Main             ( /home/optimight/baby.hs, interpreted )  

/home/optimight/baby.hs:96:1:  
    Non type-variable argument in the constraint: Show String  
    (Use -XFlexibleContexts to permit this)  
    In the type signature for `tellCar':  
      tellCar :: Show String => Car String String a -> String  
Failed, modules loaded: none.  

Answer 1

tellCar :: (Show a) => Car String String a -> String

Keep in mind the meaning of Show a here is saying:

In the type specification that follows the =>, a should have an instance for Show.

This means the third argument to the Car data constructor must be some type with a Show instance.

Specifying (Show Car) => … or (Show String) => … is meaningless; those concrete types may or may not have instances for Show (they both do, in this case), but it doesn't elucidate the actual type Car String String a -> String any.

Specifying (Show z) => … is saying:

In the type specification that follows the =>, z should have an instance for Show.

Note that the type that follows is Car String String a -> String and we can conclude that a) z is never mentioned, so we can ignore the (Show z) => …, and b) a is polymorphic without constraint! (i.e. you can't rely on it having any particular typeclass instance, including Show)

Answer 2

Main idea: Each constraint listed before the => in the type signature is there to constrain one or more type-variables to the right of the => in the type signature.

Principle: Constraints in type signatures always have a type variable in them somewhere.

Writing Show String => or Show Car => is not helpful, and the error message tells you this is because String has no type-variable (which always start with a lower-case letter). This is because either instance Show String is visible in the scope of tellCar or it is not, and you never need to list fully concrete instances as contraints in the type.

Principle: The constraint you list has to mention at least one of the type variable to the right of the => in the type signature. With LANGUAGE extensions the constraint may mention zero or more extra type variables that only exist on the left of the => in the type signature.

Writing tellCar :: Show z => Car String String a -> String violates this since a is the only type variable on the RHS of the => and Show z does not mention a. This Show z does not constrain the type variable a.

More specifically for your case you write deriving (Show) which auto-generated an instance:

instance (Show p, Show q, Show r) => Show (Car p q r) where
  showsPrec = ...

The auto-generated code only works if there are Show instances for p,q,r. Your specialization to

tellCar :: (Show a) => Car String String a -> String

mentions Car String String a. Using Show on Car String String a in tellCar selects the auto-generated instance for Show (Car p q r) and creates a need for Show String and Show a. The compiler then sees an instance for Show String from the implicitly imported Prelude module leaving only the dangling Show a constraint. This constraint on a infects the type of tellCar.

The resource to learn about the Haskell type system is one of the books on Haskell.

EDIT: The precise part of the Haskell 98 Report covering this seems to section 4.1.3. More background is in "A History of Haskell".

Answer 3

You only ever need a constraint for polymorphic type variables, because the function doesn't know what the type is going to be, and you are giving the compiler the minimum information that lets it know it will work.

Show Car => (or Show String) doesn't really mean anything as a constraint. The compiler already knows that Car p q r has a Show instance. And if Car p q r did not have a Show instance then the compiler would know that already too! So if this constraint were permitted it would either be redundant or contradictory.

The error for Show z is there to help you. You are constraining a variable that isn't being used in the type signature, so it's almost certainly a mistake.