[GHC] #8705: Type inference regression with local dictionaries

[GHC]

#8705: Type inference regression with local dictionaries
-------------------------------------------+-------------------------------
       Reporter:  goldfire                 |             Owner:
           Type:  bug                      |            Status:  new
       Priority:  normal                   |         Milestone:
      Component:  Compiler (Type checker)  |           Version:  7.7
       Keywords:                           |  Operating System:
   Architecture:  Unknown/Multiple         |  Unknown/Multiple
     Difficulty:  Unknown                  |   Type of failure:
     Blocked By:                           |  None/Unknown
Related Tickets:                           |         Test Case:
                                           |          Blocking:
-------------------------------------------+-------------------------------
 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
 [https://github.com/goldfirere/singletons/blob/master/Test/InsertionSortImp.hs
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8705>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler