Opened 6 years ago

Closed 6 years ago

Last modified 3 years ago

#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 Changed 6 years ago by goldfire

Resolution: invalid
Status: newclosed

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 assuredly not 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 does equal 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 is

type family Looper b
type instance Looper b = Looper b -> Looper b

So, 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.

comment:2 in reply to:  1 Changed 6 years ago by nh2

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 goldfire

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:4 Changed 6 years ago by Simon Peyton Jones <simonpj@…>

In ff3d07addf6af962c4d0e69d2ac02218643046d1/ghc:

Improve TcSimplify.approximateWC, fixing Trac #8155

See Note [ApproximateWC]

comment:5 Changed 6 years ago by Simon Peyton Jones <simonpj@…>

comment:6 Changed 6 years ago by simonpj

Resolution: invalid
Status: closednew

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 simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed_types/should_fail/T8155

comment:8 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In a94b4847/ghc:

Back-pedal the fix for Trac #8155

I implemented a rather elaborate fix for #8155 ages ago, which
which turns out to be
  a) unnecesssary in this particular case
  b) harmful to the defaulting story; see comment:15 of #12923.

So this patch reverts the elaborate bit. The bit I removed is
described in "Historical note" under Note [approximateWC].
Note: See TracTickets for help on using tickets.