Opened 3 years ago

Closed 3 years ago

Last modified 2 years ago

#10226 closed bug (duplicate)

Regression in constraint solver from 7.8 to 7.10

Reported by: edsko Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.10.1
Keywords: Cc: adamgundry, jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T10226
Blocked By: Blocking:
Related Tickets: #10009 Differential Rev(s):
Wiki Page:

Description

Best explained by example:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-} -- only necessary in 7.10
{-# LANGUAGE FlexibleContexts #-}    -- necessary for showFromF' example

type family F    a
type family FInv a

-- This definition is accepted in 7.8 without anything extra, but requires
-- AllowAmbiguousTypes in 7.10 (this, by itself, is not a problem):
showFromF :: (Show a, FInv (F a) ~ a) => F a -> String
showFromF fa = undefined

-- Consider what happens when we attempt to call `showFromF` at some type b.
-- In order to check that this is valid, we have to find an a such that
--
-- > b ~ F a /\ Show a /\ FInv (F a) ~ a
--
-- Introducing an intermeidate variable `x` for the result of `F a` gives us
--
-- > b ~ F a /\ Show a /\ FInv x ~ a /\ F a ~ x
--
-- Simplifying
--
-- > b ~ x /\ Show a /\ FInv x ~ a /\ F a ~ x
--
-- Set x := b
--
-- > Show a /\ FInv b ~ a /\ F a ~ b
--
-- Set a := FInv b
--
-- > Show (FInv b) /\ FInv b ~ FInv b /\ F (FInv b) ~ b
--
-- Simplifying
--
-- > Show (FInv b) /\ F (FInv b) ~ b
--
-- Indeed, we can give this definition in 7.8, but not in 7.10:
showFromF' :: (Show (FInv b), F (FInv b) ~ b) => b -> String
showFromF' = showFromF

{-------------------------------------------------------------------------------
  In 7.10 the definition of showFromF' is not accepted, but it gets stranger.
  In 7.10 we cannot _call_ showFromF at all all, even at a concrete type. Below
  we try to call it at type b ~ Int. It would need to show

  > Show (FInv Int) /\ F (FInt Int) ~ Int

  all of which should easily get resolved, but somehow don't.
-------------------------------------------------------------------------------}

type instance F    Int = Int
type instance FInv Int = Int

test :: String
test = showFromF (0 :: Int)

Change History (5)

comment:1 Changed 3 years ago by adamgundry

Cc: adamgundry added

comment:2 Changed 3 years ago by jstolarek

Cc: jstolarek added

comment:3 Changed 3 years ago by edsko

Resolution: duplicate
Status: newclosed

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

In d4a926ba52fbbbdeaadfff7c86e7175c8cc1b97c/ghc:

Test Trac #10226

Fixed by the patch for #10009

comment:5 Changed 2 years ago by simonpj

Test Case: indexed-types/should_compile/T10226
Note: See TracTickets for help on using tickets.