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,253
    • Issues 5,253
    • 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
  • #16365
Closed
Open
Issue created Feb 26, 2019 by Ryan Scott@RyanGlScottMaintainer

Inconsistency in quantified constraint solving

Consider the following program:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind
import Data.Proxy

class C a where
  m :: a -> ()

data Dict c = c => Dict

-----

type family F a :: Type -> Type
class    C (F a b) => CF a b
instance C (F a b) => CF a b

works1        :: (forall z. CF a z) => Proxy (a, b) -> Dict (CF a b)
works1 _ = Dict

works2        :: (          CF a b) => Proxy (a, b) -> Dict (C (F a b))
works2 _ = Dict

works3, fails :: (forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b))
works3 p | Dict <- works1 p = Dict
fails _ = Dict

fails, as its name suggests, fails to typecheck:

$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:33:11: error:
    • Could not deduce (C (F a b)) arising from a use of ‘Dict’
      from the context: forall z. CF a z
        bound by the type signature for:
                   fails :: forall a b.
                            (forall z. CF a z) =>
                            Proxy (a, b) -> Dict (C (F a b))
        at Bug.hs:31:1-71
    • In the expression: Dict
      In an equation for ‘fails’: fails _ = Dict
   |
33 | fails _ = Dict
   |           ^^^^

But I see no reason why this shouldn't typecheck. After all, the fact that works1 typechecks proves that GHC's constraint solver is perfectly capable of deducing that (forall z. CF a z) implies (CF a b), and the fact that works2 typechecks proves that GHC's constraint solver is perfectly capable of deducing that (CF a b) implies that (C (F a b)). Why then can GHC's constraint solver not connect the dots and deduce that (forall z. CF a z) implies (C (F a b)) (in the type of fails)?

Note that something with the type (forall z. CF a z) => Proxy (a, b) -> Dict (C (F a b)) //can// be made to work if you explicitly guide GHC along with explicit pattern-matching on a Dict, as works3 demonstrates. But I claim that this shouldn't be necessary.

Moreover, in this variation of the program above:

-- <as above>
-----

data G a :: Type -> Type
class    C (G a b) => CG a b
instance C (G a b) => CG a b

works1' :: (forall z. CG a z) => Proxy (a, b) -> Dict (CG a b)
works1' _ = Dict

works2' :: (          CG a b) => Proxy (a, b) -> Dict (C (G a b))
works2' _ = Dict

works3' :: (forall z. CG a z) => Proxy (a, b) -> Dict (C (G a b))
works3' _ = Dict

works3' needs no explicit Dict pattern-matching to typecheck.

Trac metadata
Trac field Value
Version 8.6.3
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
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