[Haskell-cafe] overlapping/Incoherent closed type families

[Silvio Frischknecht]

Hi

I have been playing around a bit with closed type families. However, I somehow 
always bump my head at the fact that things usually doesn't work for Num 
without specifying the type.

Here is an example.

    {-# LANGUAGE FlexibleInstances         #-}
    {-# LANGUAGE FlexibleContexts          #-}
    {-# LANGUAGE TypeFamilies              #-}
    {-# LANGUAGE DataKinds                 #-}
    {-# LANGUAGE UndecidableInstances      #-}
    {-# LANGUAGE OverlappingInstances      #-}
    {-# LANGUAGE IncoherentInstances       #-}
    module Main where

    import Data.Typeable

    type family UnMaybed a where
        UnMaybed (Maybe a) = a
        UnMaybed a = a

    class UnMaybe x where
        unMaybe :: x -> UnMaybed x

    instance UnMaybe (Maybe a) where
        unMaybe (Just a) = a

    instance (UnMaybed a ~ a) => UnMaybe a where
        unMaybe a = a

    main = do
        print $ unMaybe 'c'
        print $ unMaybe (1::Int)
        print $ unMaybe (Just 1)
        print $ unMaybe 1 -- this line does not compile

everything except the last line will compile.

    ../Example.hs:23:17:
        Occurs check: cannot construct the infinite type: s0 ~ UnMaybed s0
        The type variable ‘s0’ is ambiguous
        In the second argument of ‘($)’, namely ‘unMaybe 1’
        In a stmt of a 'do' block: print $ unMaybe 1

Now I know this is because numbers are polymorphic and (Maybe a) could be an 
instance of Num. I think for normal overlapping typeclasses this dilemma can 
be solved by using the IncoherentInstances PRAGMA. Anyway, I wanted to ask if 
there is a way to make this work in type families?

I also thought about specifying Num explicitly in UnMaybed

    type family UnMaybed a where
        unMaybed (Num a => a) = a
        UnMaybed (Maybe a) = a
        UnMaybed a = a

This compiles but i think the first case will never be matched this is probably 
a bug.

Silvio