[Haskell-cafe] overlapping/Incoherent closed type families

[Richard Eisenberg]

Hi Silvio,

Yes, you've hit upon a limitation of closed type families, but the limitation is there for good reason.

IncoherentInstances threatens coherence of type class instances, meaning that a constraint `UnMaybe <<some type>>` might be fulfilled differently in different places, even for the same <<some type>>. But, type class instance selection is purely a runtime-behavior effect. Choosing a different instance cannot affect the types in your program.

Type families, on the other hand, directly affect the types. Allowing incoherence like the way IncoherentInstances works could be used to implement unsafeCoerce.

So, I'm afraid you're out of luck. I've hit this exact same problem in my own work, and there's not much of a way around it without a type signature. (One possibility is to use RebindableSyntax essentially to disable number overloading, but that's a bit of a big hammer.)

The fact that your last example (with UnMaybed (Num a => a)) even compiles is very much a bug that I will file shortly.

I hope this explanation is helpful!
Richard

On Mar 15, 2014, at 10:21 AM, Silvio Frischknecht wrote:

> 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
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>