## #8155 closed bug (fixed)

# Defaulting bug or unfortunate error message with closed type families

Reported by: | nh2 | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 7.6.3 |

Keywords: | Cc: | mail@… | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | indexed_types/should_fail/T8155 |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

https://github.com/nh2/infinite-type-families/blob/master/Test2.hs

Some code extracted from hmatrix:

{-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleInstances #-} module Test where data Vector a = Vector a data Matrix a = Matrix a class Build f where build' :: BoundsOf f -> f -> ContainerOf f #if __GLASGOW_HASKELL__ <= 706 -- Normal type families with GHC 7.6, works well. type family BoundsOf x type instance BoundsOf (a->a) = Int type instance BoundsOf (a->a->a) = (Int,Int) type family ContainerOf x type instance ContainerOf (a->a) = Vector a type instance ContainerOf (a->a->a) = Matrix a #else -- Closed type families for GHC 7.8 type family BoundsOf x where BoundsOf (a->a->a) = (Int,Int) BoundsOf (a->a) = Int type family ContainerOf x where ContainerOf (a->a) = Vector a ContainerOf (a->a->a) = Matrix a #endif instance (Num a) => Build (a->a) where build' = buildV buildV :: (Integral a, Num b) => a -> (b -> c) -> Vector c buildV _ _ = undefined

This is probably related to #8154.

With GHC 7.7, we get the following error:

Test2.hs:59:14: Could not deduce (BoundsOf (a -> a) ~ Integer) from the context (Num a) bound by the instance declaration at Test2.hs:58:10-32 Expected type: BoundsOf (a -> a) -> (a -> a) -> ContainerOf (a -> a) Actual type: Integer -> (a -> a) -> Vector a Relevant bindings include build' :: BoundsOf (a -> a) -> (a -> a) -> ContainerOf (a -> a) (bound at Test2.hs:59:5) In the expression: buildV In an equation for ‛build'’: build' = buildV

1) Where does this Integer come from?

2) Change

BoundsOf (a->a) = Int

into

BoundsOf (a->a) = Integer

You get the same error message, although clearly

`BoundsOf (a -> a) ~ Integer`

(you just wrote that down).

Even if the order matters in closed type families, is this not the wrong error message?

3) If you flip the order so that the (a->a) case comes first, it works (with both it Int or Integer). I don't quite understand why.

### Change History (8)

### comment:1 follow-up: 2 Changed 6 years ago by

Resolution: | → invalid |
---|---|

Status: | new → closed |

### comment:2 Changed 6 years ago by

Replying to goldfire:

This may be an infelicity in defaulting (which I'm not terribly familiar with)

[...]

I will close this ticket, but do please reopen if you can characterize the bug as a specific infelicity in the defaulting mechanism.

I know too little about how defaulting works, we would need somebody who understands that.

This is all very subtle and can be unexpected, but after lots and lots of thinking, Simon PJ, Dimitrios V, and I could not come up with a better way here

I am not saying that I find this behaviour of closed type families wrong or so.

Is it not possible to change the generated error message to give a hint why this is rejected, e.g. based on what you explained here?

I understand your reasoning here, but had I not seen your example here and would I encounter this message in GHC with the current error message, chances are high I'd think it's a bug.

### comment:3 Changed 6 years ago by

It's hard for me to see how to do this. It seems that the problem is that your closed type family contains an equation which does not fire in the general case. But, this equation does fire in more specific cases, when the type variable is fully instantiated. I could imagine issuing a warning in this situation, but it would seem that this isn't always a programmer mistake. I could also imagine tracking when you have an equation like this that doesn't fire and then reporting that to the user along with other type errors, in case those errors are related. But, that would take a fair amount of very specific plumbing to pull together, and it's not obvious that this is the right idea.

Do you see a better way forward here? What should be reported and when?

### comment:6 Changed 6 years ago by

Resolution: | invalid |
---|---|

Status: | closed → new |

Thank you for identifying this problem. Once I understood it, the fix was easy. New error message is much more sensible

T8155.hs:26:14: Could not deduce (Integral (BoundsOf (a -> a))) arising from a use of ‛buildV’ from the context (Num a) bound by the instance declaration at T8155.hs:25:10-32 In the expression: buildV In an equation for ‛build'’: build' = buildV In the instance declaration for ‛Build (a -> a)’

Simon

### comment:7 Changed 6 years ago by

Resolution: | → fixed |
---|---|

Status: | new → closed |

Test Case: | → indexed_types/should_fail/T8155 |

**Note:**See TracTickets for help on using tickets.

This may be an infelicity in defaulting (which I'm not terribly familiar with), but the closed-type-family behavior is correct, if rather subtle and confusing.

The original post says "clearly

`BoundsOf (a -> a) ~ Integer`

(you just wrote that down)". I would say that that's not exactly what was written. What the closed-type-family definition of`BoundsOf`

says is that`BoundsOf (a -> a) ~ Integer`

as long as`a`

is most assuredlynot`a -> a`

. That is, GHC must be sure that previous equations of a closed type family can never apply before using a given equation. Because it is quite possible that`a`

will be instantiated at a type such that`a`

doesequal`a -> a`

(see below), GHC will not use the second equation to simplify`BoundsOf (a -> a)`

.The dangerous type that

`a`

might be instantiated with isSo, unless GHC knows that

`a`

won't be instantiated at a type like`Looper`

, the second equation will not be used. As a concrete example of this, GHC will happily reduce`BoundsOf (Bool -> Bool)`

.This is all very subtle and can be unexpected, but after lots and lots of thinking, Simon PJ, Dimitrios V, and I could not come up with a better way here. When I wrote a suggested implementation of

`BoundsOf`

in my response to #8154, I thought a little while about the ordering of the equations to avoid exactly this problem.I will close this ticket, but do please reopen if you can characterize the bug as a specific infelicity in the defaulting mechanism.