Opened 3 months ago

Closed 8 weeks ago

#8705 closed bug (fixed)

Type inference regression with local dictionaries

Reported by: goldfire Owned by:
Priority: high Milestone: 7.8.1
Component: Compiler (Type checker) Version: 7.8.1-rc1
Keywords: Cc: jan.stolarek@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: polykinds/T8705 Blocked By:
Blocking: Related Tickets:

Description

Consider this code:

{-# LANGUAGE ScopedTypeVariables, TypeOperators, DataKinds,
             MultiParamTypeClasses, GADTs, ConstraintKinds #-}

import Data.Singletons.Prelude
import GHC.Exts

data Dict c where
  Dict :: c => Dict c

-- A less-than-or-equal relation among naturals
class a :<=: b

sLeq :: Sing n -> Sing n2 -> Dict (n :<=: n2)
sLeq = undefined

insert_ascending :: forall n lst n1.
  (lst ~ '[n1]) => Proxy n1 -> Sing n -> SList lst -> Dict (n :<=: n1)
insert_ascending _ n lst =
  case lst of -- If lst has one element...
      SCons h _ -> case sLeq n h of -- then check if n is <= h
        Dict -> Dict -- if so, we're done

(adapted from this file)

GHC 7.6.3 compiles without incident. When I run HEAD (with -fprint-explicit-kinds), I get

Ins.hs:25:17:
    Could not deduce (n :<=: n1) arising from a use of ‛Dict’
    from the context ((~) [*] lst ((':) * n1 ('[] *)))
      bound by the type signature for
                 insert_ascending :: (~) [*] lst ((':) * n1 ('[] *)) =>
                                     Proxy * n1 -> Sing * n -> SList * lst -> Dict (n :<=: n1)
      at Ins.hs:(20,21)-(21,70)
    or from ((~) [*] lst ((':) * n0 n2))
      bound by a pattern with constructor
                 SCons :: forall (a0 :: BOX) (z0 :: [a0]) (n0 :: a0) (n1 :: [a0]).
                          (~) [a0] z0 ((':) a0 n0 n1) =>
                          Sing a0 n0 -> Sing [a0] n1 -> Sing [a0] z0,
               in a case alternative
      at Ins.hs:24:7-15
    or from (n :<=: n0)
      bound by a pattern with constructor
                 Dict :: forall (c :: Constraint). (c) => Dict c,
               in a case alternative
      at Ins.hs:25:9-12
    Possible fix:
      add (n :<=: n1) to the context of
        the data constructor ‛Dict’
        or the data constructor ‛SCons’
        or the type signature for
             insert_ascending :: (~) [*] lst ((':) * n1 ('[] *)) =>
                                 Proxy * n1 -> Sing * n -> SList * lst -> Dict (n :<=: n1)
    In the expression: Dict
    In a case alternative: Dict -> Dict
    In the expression: case sLeq n h of { Dict -> Dict }

If you stare at the type error long enough, you will see that GHC should be able to type-check this. The test case requires singletons-0.9.x, but is already much reduced.

Interestingly, if all the "givens" are put in the top-level type signature, GHC does its job well. It seems that the act of unpacking the dictionaries is causing the problem.

Change History (9)

comment:1 Changed 3 months ago by jstolarek

  • Cc jan.stolarek@… added

comment:2 Changed 2 months ago by goldfire

  • Milestone set to 7.8.1
  • Priority changed from normal to high
  • Version changed from 7.7 to 7.8.1-rc1

Tweaking settings on the ticket to give it perhaps higher visibility. This bug is a type inference regression that I believe will hit the type system power users and would be embarrassing if we don't fix before the release. I've confirmed that the error happens in 7.8rc1.

I haven't put time into looking for the source of the problem, but I think it will be in code I'm not (yet) deeply familiar with. If the release is approaching and this is still around, please ping me and I'll see what I can do.

comment:3 Changed 2 months ago by simonpj

Just to check, we have three givens:

G1:   lst ~ n1 : []
G2:   lst ~ n0 : n2
G3:   n :<=: n2

From the G1,G2 we find n1 ~ n0, and from that and G3 we get n :<=: n1, which is what we want to prove.

Is that the reasoning?

Would it be difficult to drop the dependence on singletons, or include the code from there that's needed directly into this module?

Simon

comment:4 Changed 2 months ago by goldfire

Your text is correct, but your code is not. I believe you meant

G1:   lst ~ n1 : []
G2:   lst ~ n0 : n2
G3:   n :<=: n0

Note the n0 in the last line. Otherwise, yes, I agree with your comment.

I'll try to reduce the case more, yes.

comment:5 Changed 2 months ago by goldfire

Here is a version without the singletons dependency:

{-# LANGUAGE TypeOperators, DataKinds, PolyKinds,
             MultiParamTypeClasses, GADTs, ConstraintKinds, TypeFamilies #-}

module Bug where

data family Sing (a :: k)
data Proxy a = Proxy

data instance Sing (a :: Maybe k) where
  SJust :: Sing h -> Sing (Just h)

data Dict c where
  Dict :: c => Dict c

-- A less-than-or-equal relation among naturals
class a :<=: b

sLeq :: Sing n -> Sing n2 -> Dict (n :<=: n2)
sLeq = undefined

insert_ascending :: (lst ~ Just n1) => Proxy n1 -> Sing n -> Sing lst -> Dict (n :<=: n1)
insert_ascending _ n (SJust h) =
  case sLeq n h of 
    Dict -> Dict

Interestingly, when I tried getting rid of the data family, the code started compiling. Perhaps there's a problem with normalisation somewhere?

comment:6 Changed 2 months ago by simonpj

Aha. Got it. Thank you. Patch coming

comment:7 Changed 2 months ago by Simon Peyton Jones <simonpj@…>

In 89d2c048c81020a701ac94d949b4d6f1ced37cfa/ghc:

Keep kind-inconsistent Given type equalities (fixes Trac #8705)

I was too eager when fixing Trac #8566, and dropped too many
equalities on the floor, thereby causing Trac #8705.

The fix is easy: delete code.  Lots of new comments!

comment:8 Changed 2 months ago by simonpj

  • Status changed from new to merge
  • Test Case set to polykinds/T8705

comment:9 Changed 8 weeks ago by thoughtpolice

  • Resolution set to fixed
  • Status changed from merge to closed

Merged.

Note: See TracTickets for help on using tickets.