[Haskell-cafe] question about type constructors

[Roman Cheplyaka]

* TP <paratribulations at free.fr> [2013-05-23 00:34:57+0200]
> Hi,
> 
> In the program I am trying to write, I have a problem that can be reduced to 
> the following dummy example:
> 
> --------------------------
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE IncoherentInstances #-}
> 
> class PrettyPrint a where
>     prettify :: a -> String
> 
> data Gender = Male | Female | Gender3 | Gender4
> 
> data Person :: Gender -> * where
>     Person :: String -> Person b
>     Child :: String -> Person a -> Person b -> Person c
> 
> instance PrettyPrint (Person a)
> 
> instance PrettyPrint (Person Male) where
>     prettify (Person name) = "My name is " ++ (show name)
>           ++ " and I am a male"
>     prettify (Child name person1 person2) = "My name is " ++ (show name)
>           ++ " and my parents are:" ++ (prettify person1) ++ ", "
>           ++ (prettify person2)
> 
> main = do
> 
> let p1 = Person "Jim" :: Person Male
> let p2 = Person "Joe" :: Person Male
> let p3 = Child "Jack" p1 p2
> 
> print $ prettify p1
> print $ prettify p2
> print $ prettify p3
> --------------------------
> 
> The idea is that I want to implement PrettyPrint only for a subset of the 
> possible types in Gender (through promotion process). Why? It would be 
> longer to explain (it is a bit more complicated in my real program).
> 
> Anyway, in the program above, I have found that with IncoherentInstances 
> (and the empty instance definition for (Person a)), it is working, it is 
> able to use the most specific instance corresponding to the current type (I 
> don't know exactly why). For example, p1 and p2 are correctly printed above, 
> because they are of type (Person Male) and because I have implemented 
> PrettyPrint for (Person Male).
> 
> But it does not work for p3, I obtain an error at runtime:
> -----
> $ runghc test.hs
> "My name is \"Jim\" and I am a male"
> "My name is \"Joe\" and I am a male"
> test_typelost.hs: test_typelost.hs:16:10-31: No instance nor default method 
> for class operation Main.prettify
> -----
> 
> The reason is that the information that p1 and p2 are Male seems to be 
> "lost" when we construct the child "Child "Jack" p1 p2", probably because 
> GHC only sees that in the type signature of Child, we have a more general 
> (Person a) -> (Person b). So he tries to find an implementation of prettify 
> in PrettyPrint (Person a), but there is none.
> 
> Is there any workaround?

The rule of thumb is that you should never use IncoherentInstances.

The proper way to do it is:

  data Person :: Gender -> * where
      Person :: String -> Person b
      Child
        :: (PrettyPrint a, PrettyPrint b)
        => String -> Person a -> Person b -> Person c

Roman