Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,246
    • Issues 5,246
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 564
    • Merge requests 564
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #8705
Closed
Open
Issue created Jan 27, 2014 by Richard Eisenberg@raeDeveloper

Type inference regression with local dictionaries

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking