[Haskell-cafe] overlapping/Incoherent closed type families

[jberryman]

On Saturday, March 15, 2014 10:21:36 AM UTC-4, 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
> Haskel... at haskell.org <javascript:>
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

I'm glad Richard Eisenberg responded here; I was going to point you to 
https://ghc.haskell.org/trac/ghc/wiki/NewAxioms with the caveat that I 
don't totally understand the details there.

A couple things about your example: you actually don't need 
IncoherentInstances here; OverlappingInstances is sufficient, since the 
instance head  `UnMaybe (Maybe a)` is more precise than `UnMaybe a`. 
Personally I'm *much* more comfortable with just OverlappingInstances than 
IncoherentInstances.

The other thing to consider is that the only reason why e.g. `print 1` even 
compiles is because of defaulting rules, which are something of a hack. 
Maybe that makes you feel better about living with the limitation in your 
current code.

Brandon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140315/52f5cf82/attachment.html>