Opened 3 years ago

Closed 3 years ago

Last modified 2 years ago

#10177 closed bug (fixed)

Typeable solver regression

Reported by: glguy Owned by:
Priority: highest Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.1-rc3
Keywords: Cc: diatchki
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: testsuite/tests/typecheck/should_compile/T10177
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This bug is known and fixed in master. Simon and Austin and Iavor are all aware of it. This ticket exists to ensure that the fix doesn't get lost.

This code breaks under the Typeable solver in 7.10.1-rc3 and is fixed in master.

The relevant commit in master is 3a0019e3672097761e7ce09c811018f774febfd2 : Improve Typeable solver.

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
module Bug where

import Data.Typeable

newtype V n a = V [a]

class    Typeable a                   => C a
instance (Typeable (V n), Typeable a) => C (V n a)

-- Bug.hs:13:10:
--  Could not deduce (Typeable (V n a))
--    arising from the superclasses of an instance declaration
--  from the context (Typeable (V n), Typeable a)
--    bound by the instance declaration at Bug.hs:13:10-50
--  In the instance declaration for ‘C (V n a)’

Change History (12)

comment:1 Changed 3 years ago by glguy

Resolution: fixed
Status: newclosed

I just saw this was merged

comment:2 Changed 3 years ago by hvr

comment:3 Changed 3 years ago by Austin Seipp <austin@…>

In 854fd12358fef51848c2eb5e7e08d9c8cec43e16/ghc:

testsuite: add test for #10177

Signed-off-by: Austin Seipp <austin@well-typed.com>

comment:4 Changed 3 years ago by thoughtpolice

Test Case: testsuite/tests/typecheck/should_compile/T10177

comment:5 Changed 3 years ago by simonpj

Resolution: fixed
Status: closednew

Actually I really don't think this code should work. It should be

instance (Typeable n, Typeable a) => C (V n a)

Otherwise there is an overlap between the given (Typeable (V n)) and the built-in instance for Typeable (V n a). Making the code given here work is very fragile, and might depend on solve order.

I vote that should fail. Any dissenters?

Simon

comment:6 Changed 3 years ago by goldfire

What about this?

instance (Typeable a, Typeable b) => C (a b)

That looks good to me. But what you have above is just a simple substitution on my instance, so I think it should be good.

Can the Typeable solver just immediately decompose Typeable (V n) to Typeable n? Is there a threat that the overlapping instances are semantically different?

comment:7 Changed 3 years ago by diatchki

I don't think that there is anything wrong here, so I think that we should accept the program.

The (new, now merged) Typeable solver does exactly what Richard says.

The instance for Typeable (f a) has to be computed from the evidence for the types f and a. If that was not the case, we'd get some very odd behavior depending on how type variables get instantiated. Now, if f happened to be a concrete type (e.g., like V n), then we can reduce further, but if we happen to already have a solution for V n, we don't have to reduce any further---after all, that solution must have been built by the internal typeable solver in the first place.

Note that the actual TypeReps are built by always applying the constructor to all arguments: see the comment on mkAppTy in Data.Typeable.Internal.

comment:8 Changed 3 years ago by hvr

Milestone: 7.10.17.10.2

GHC 7.10.1 was just released, so any change can occur in milestone:7.10.2 earliest (if it turns out there's nothing to change, please revert back to the 7.10.1 milestone)

comment:9 Changed 3 years ago by simonpj

Austin: check that this works on the 7.10 branch; assuming that it does, re-milestone for 7.12.

Simon

comment:10 Changed 3 years ago by thoughtpolice

Milestone: 7.10.27.12.1

Confirmed working on 7.10.1, so we can punt this.

comment:11 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed

Actually it's fine in HEAD and should stay that way, i.e. NOT as I said in comment:5.

See Note [Instance and Given overlap] in TcInteract.

I'll close as fixed.

comment:12 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

Note: See TracTickets for help on using tickets.