Opened 4 years ago

Last modified 20 months ago

#4295 new bug

Review higher-rank and impredicative types

Reported by: simonpj Owned by: simonpj
Priority: normal Milestone: 7.6.2
Component: Compiler Version: 6.12.3
Keywords: Cc: nicolas.pouillard@…, v.dijk.bas@…, hackage.haskell.org@…, favonia@…, nathanhowell@…, rabeslik@…, ben@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty:
Test Case: Blocked By:
Blocking: Related Tickets:

Description (last modified by simonpj)

The ticket is a placeholder to remind me to work through the test cases for impredicative and higher rank types in the new typechecker. For now, I'm marking many of them as expect_broken on this ticket, although I think many of them really should fail.

  • tc150
  • tc194
  • tcfail198
  • tcfail174
  • tcfail165
  • tcfail145
  • tcfail104
  • tc211
  • indexed-types/should_compile/T4120
  • simpl017
  • Many tests in boxy/ (see also #1330 for Church2)
  • #2193
  • #2846
  • #4347
  • Lennart's blog post has an interesting use case of impredicative polymorphism; it worked in 7.0, but alas not in the new typechecker.

Change History (21)

comment:1 Changed 4 years ago by simonpj

  • Description modified (diff)

comment:2 Changed 4 years ago by simonpj

  • Description modified (diff)
  • Summary changed from Review impredicative types to Review higher-rank and impredicative types

comment:3 Changed 4 years ago by simonpj

  • Description modified (diff)

comment:4 Changed 4 years ago by simonpj

  • Description modified (diff)

comment:5 Changed 4 years ago by simonpj

  • Description modified (diff)

comment:6 Changed 4 years ago by simonpj

  • Description modified (diff)

comment:7 Changed 4 years ago by simonpj

  • Description modified (diff)

comment:8 Changed 4 years ago by igloo

  • Milestone set to 7.2.1
  • Owner set to simonpj

comment:9 Changed 3 years ago by simonpj

Here's an example from Bas van Dijk that needs a rigid type signature:

{-# LANGUAGE UnicodeSyntax
           , KindSignatures
           , RankNTypes
           , MultiParamTypeClasses
           , FunctionalDependencies
  #-}

module Bas where

import Data.List (find)

data Ctx = Ctx
data Device = Device
data DeviceDesc = DeviceDesc

data RegionalDeviceHandle (r ∷ * → *) = RegionalDeviceHandle 
data RegionT s (pr ∷ * → *) α = RegionT

instance Monad pr ⇒ Monad (RegionT s pr) where
    return = undefined
    (>>=)  = undefined

runRegionT ∷ (∀ s. RegionT s pr α) → pr α
runRegionT = undefined

openDevice ∷ Device → RegionT s pr (RegionalDeviceHandle (RegionT s pr)) 
openDevice = undefined

withDevice ∷ Monad pr
           ⇒ Device
           → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
           → pr α
withDevice dev f = runRegionT $ openDevice dev >>= f

withDeviceWhich ∷ ∀ pr α
                . Monad pr
                ⇒ Ctx
                → (DeviceDesc → Bool)
                → (∀ s. RegionalDeviceHandle (RegionT s pr) → RegionT s pr α)
                → pr α
withDeviceWhich ctx p f = do devs ← return [Device]
                             useWhich devs withDevice p f

useWhich ∷ ∀ k desc e (m ∷ * → *) α
         . (GetDescriptor e desc)
         ⇒ [e]
         → (e → k → m α)
         → (desc → Bool)
         → k
         → m α
useWhich ds w p f = case find (p . getDesc) ds of
                      Nothing → error "not found"
                      Just d  → w d f

class GetDescriptor α desc | α → desc, desc → α where
    getDesc ∷ α → desc

instance GetDescriptor Device DeviceDesc where
    getDesc = undefined

See the thread at http://www.mail-archive.com/glasgow-haskell-users@haskell.org/index.html#18905

comment:10 Changed 3 years ago by ertai

  • Cc nicolas.pouillard@… added

comment:11 Changed 3 years ago by basvandijk

  • Cc v.dijk.bas@… added

comment:12 Changed 3 years ago by liyang

  • Cc hackage.haskell.org@… added

comment:13 Changed 3 years ago by Favonia

  • Cc favonia@… added

comment:14 Changed 3 years ago by nathanhowell

  • Cc nathanhowell@… added

comment:15 Changed 3 years ago by simonpj

  • Description modified (diff)

comment:16 Changed 3 years ago by simonpj

  • Description modified (diff)

comment:17 Changed 3 years ago by beroal

  • Cc rabeslik@… added

comment:18 Changed 2 years ago by simonpj

See also #5596 (impredicative).

comment:19 Changed 2 years ago by igloo

  • Milestone changed from 7.4.1 to 7.6.1

comment:20 Changed 2 years ago by benmos

  • Cc ben@… added

Just a note that I've also been tripped up by #5596. (I was initially very puzzled why my own version of ($) copied and pasted from Prelude with the same pragmas didn't work the same as the built-in one...)

comment:21 Changed 20 months ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2
Note: See TracTickets for help on using tickets.