Skip to content

GitLab

  • Menu
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 4,869
    • Issues 4,869
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 458
    • Merge requests 458
  • 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 Compiler
  • GHCGHC
  • Issues
  • #9898
Closed
Open
Created Dec 18, 2014 by erisco@trac-erisco

Wanted: higher-order type-level programming

'test3' is expected to type check given that 'test1' and 'test2' type check. 'test4' is not expected to type check.

ghc_bug2.hs:24:9:
    Couldn't match type `(Char, ())' with `()'
    Expected type: Filter (Equal Int) (Char, Filter (Equal Int) ())
      Actual type: ()
    In the expression:
        () :: Filter (Equal Int) (Char, Filter (Equal Int) ())
    In an equation for `test2':
        test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())

ghc_bug2.hs:28:9:
    Couldn't match type `(Char, ())' with `()'
    Expected type: Filter (Equal Int) (Char, ())
      Actual type: ()
    In the expression: ()
    In an equation for `test3': test3 = ()
{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds #-}
module Main where

type family Filter f xs where
  Filter f (x, xs) = ApplyFilter (f x) (x, Filter f xs)
  Filter f () = ()
--

type family ApplyFilter p xs where
  ApplyFilter False (x, xs) = xs
  ApplyFilter p xs = xs
--

type family Equal x y where
  Equal x x = True
  Equal x y = False
--

-- Type checks
test1 :: ApplyFilter ((Equal Int) Char) (Char, Filter (Equal Int) ())
test1 = ()

-- Couldn't match type `(Char, ())' with `()'
test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())

-- Couldn't match type `(Char, ())' with `()'
test3 :: Filter (Equal Int) (Char, ())
test3 = ()

-- Type checks, should not
test4 :: Filter (Equal Int) (Char, ())
test4 = ('x', ())
Trac metadata
Trac field Value
Version 7.8.3
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system Windows
Architecture x86_64 (amd64)
Edited Mar 10, 2019 by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking