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,393
    • Issues 4,393
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 381
    • Merge Requests 381
  • 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
  • #15122

Closed
Open
Opened May 04, 2018 by fmixing@trac-fmixing

GHC HEAD typechecker regression

This code, distilled from the type-level-sets library:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

data Proxy (p :: k) = Proxy

data Set (n :: [k]) where
    Empty :: Set '[]
    Ext :: e -> Set s -> Set (e ': s)

type family (m :: [k]) :\ (x :: k) :: [k] where
     '[]       :\ x = '[]
     (x ': xs) :\ x = xs
     (y ': xs) :\ x = y ': (xs :\ x)

class Remove s t where
  remove :: Set s -> Proxy t -> Set (s :\ t)

instance Remove '[] t where
  remove Empty Proxy = Empty

instance {-# OVERLAPS #-} Remove (x ': xs) x where
  remove (Ext _ xs) Proxy = xs

instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
      => Remove (y ': xs) x where
  remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)

Typechecks in GHC 8.4.2, but not in GHC HEAD:

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

Bug.hs:31:33: error:
    • Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x))
      from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
        bound by the instance declaration at Bug.hs:(29,31)-(30,27)
      or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*]))
        bound by a pattern with constructor:
                   Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s),
                 in an equation for ‘remove’
        at Bug.hs:31:11-18
      Expected type: Set ((y : xs) :\ x)
        Actual type: Set (e : (s :\ x))
    • In the expression: Ext y (remove xs x)
      In an equation for ‘remove’:
          remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
      In the instance declaration for ‘Remove (y : xs) x’
    • Relevant bindings include
        x :: Proxy x (bound at Bug.hs:31:22)
        xs :: Set s (bound at Bug.hs:31:17)
        y :: e (bound at Bug.hs:31:15)
        remove :: Set (y : xs) -> Proxy x -> Set ((y : xs) :\ x)
          (bound at Bug.hs:31:3)
   |
31 |   remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
   |                                 ^^^^^^^^^^^^^^^^^^^

This regression was introduced in commit e3dbb44f (Fix #12919 (closed) by making the flattener homegeneous.).

Edited Mar 10, 2019 by Ryan Scott
Assignee
Assign to
8.6.1
Milestone
8.6.1 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#15122