overlapping/Incoherent closed type families
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
yeah... I dont think close type families can match on the first one, thought its interesting to ask if they should be able to.... On Sat, Mar 15, 2014 at 10:21 AM, Silvio Frischknecht < silvio.frischi@gmail.com> 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
participants (4)
-
Carter Schonwald -
jberryman -
Richard Eisenberg -
Silvio Frischknecht