Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • 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 4,843
    • Issues 4,843
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 453
    • Merge requests 453
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
    • Value stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #15122

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