Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,394
    • Issues 4,394
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 374
    • Merge Requests 374
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #18704

Closed
Open
Opened Sep 17, 2020 by rybochodonezzar@rybochodonezzar

GHC could not deduce constraint from itself

Summary

following code:

{-# LANGUAGE GADTs, DataKinds, PolyKinds, ConstraintKinds, TypeApplications, RankNTypes, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableSuperClasses, FlexibleInstances, PatternSynonyms, FlexibleContexts, AllowAmbiguousTypes, ScopedTypeVariables #-}

module Lib where

import GHC.Exts
import GHC.TypeLits
import Data.Proxy

data a ::: b = a ::: b

class Pair f where
  type Left  f :: a
  type Right f :: b

instance Pair (a '::: b) where
  type Left  (a '::: b) = a
  type Right (a '::: b) = b

class    NC (x :: k)
instance NC (x :: k)

data L1 c f xs where
  LC :: c x => f x -> L1 c f xs -> L1 c f (x ': xs)
  LN :: L1 c f '[]

class (c1 (Left f), c2 (Right f)) => PairC c1 c2 f
instance (c1 x, c2 y) => PairC c1 c2 (x '::: y)

data f1 :*: f2 :: (kx ::: ky) -> * where
  (:*:) :: f1 x -> f2 y -> (f1 :*: f2) (x '::: y)

pairC :: forall c1 c2 x y e . (c1 x, c2 y) => (PairC c1 c2 (x '::: y) => e) -> e
pairC e = e

type Foo t = L1 (PairC KnownSymbol NC) (Proxy :*: t)
pattern Foo :: forall s a t xs . KnownSymbol s => KnownSymbol s => Proxy s -> t a -> Foo t xs -> Foo t (s '::: a ': xs)
pattern Foo p t xs <- LC (p :*: t) xs where
  Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)

Results in this compile error:

/home/ryba/ghc-bug/src/Lib.hs:38:46: error:
    • Could not deduce (PairC KnownSymbol NC (s '::: a))
        arising from a use of ‘LC’
      from the context: KnownSymbol s
        bound by the signature for pattern synonym ‘Foo’
        at src/Lib.hs:(37,1)-(38,61)
      or from: PairC KnownSymbol NC (s '::: a)
        bound by a type expected by the context:
                   PairC KnownSymbol NC (s '::: a) =>
                   L1 (PairC KnownSymbol NC) (Proxy :*: t) ((s '::: a) : xs)
        at src/Lib.hs:38:45-61
    • In the fifth argument of ‘pairC’, namely ‘(LC (p :*: t) xs)’
      In the expression: pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
      In an equation for ‘Foo’:
          Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
   |
38 |   Foo p t xs = pairC @KnownSymbol @NC @s @a (LC (p :*: t) xs)
   |                                              ^^^^^^^^^^^^^^^

Which basically boils down to "could not deduce a from a"

Environment

  • GHC version used: 8.10.2
  • stack resolver=nightly-2020-09-14

Optional:

  • Operating System: Ubuntu
  • System Architecture: x86-64
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#18704