GitLab

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.

Trac metadata

Trac field	Value
Version	7.7
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture