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