Re: [Haskell-cafe] overlapping/Incoherent closed type families

15 Mar 2014

      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...@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

Re: [Haskell-cafe] overlapping/Incoherent closed type families

jberryman