Opened 6 years ago

Last modified 3 months ago

#4295 infoneeded task

Review higher-rank and impredicative types

Reported by: simonpj Owned by: simonpj
Priority: normal Milestone:
Component: Compiler (Type checker) 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 Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

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 (28)

comment:1 Changed 6 years ago by simonpj

  • Description modified (diff)

comment:2 Changed 6 years ago by simonpj

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

comment:3 Changed 6 years ago by simonpj

  • Description modified (diff)

comment:4 Changed 6 years ago by simonpj

  • Description modified (diff)

comment:5 Changed 6 years ago by simonpj

  • Description modified (diff)

comment:6 Changed 6 years ago by simonpj

  • Description modified (diff)

comment:7 Changed 6 years ago by simonpj

  • Description modified (diff)

comment:8 Changed 6 years ago by igloo

  • Milestone set to 7.2.1
  • Owner set to simonpj

comment:9 Changed 5 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 5 years ago by ertai

  • Cc nicolas.pouillard@… added

comment:11 Changed 5 years ago by basvandijk

  • Cc v.dijk.bas@… added

comment:12 Changed 5 years ago by liyang

  • Cc hackage.haskell.org@… added

comment:13 Changed 5 years ago by Favonia

  • Cc favonia@… added

comment:14 Changed 5 years ago by nathanhowell

  • Cc nathanhowell@… added

comment:15 Changed 5 years ago by simonpj

  • Description modified (diff)

comment:16 Changed 5 years ago by simonpj

  • Description modified (diff)

comment:17 Changed 5 years ago by beroal

  • Cc rabeslik@… added

comment:18 Changed 4 years ago by simonpj

See also #5596 (impredicative).

comment:19 Changed 4 years ago by igloo

  • Milestone changed from 7.4.1 to 7.6.1

comment:20 Changed 4 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 4 years ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2

comment:22 Changed 22 months ago by thoughtpolice

  • Milestone changed from 7.6.2 to 7.10.1

Moving to 7.10.1.

comment:23 Changed 16 months ago by thoughtpolice

  • Milestone changed from 7.10.1 to 7.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:24 Changed 13 months ago by thomie

  • Component changed from Compiler to Compiler (Type checker)
  • Type changed from bug to task

comment:25 Changed 8 months ago by thoughtpolice

  • Milestone changed from 7.12.1 to 8.0.1

Milestone renamed

comment:26 Changed 6 months ago by bgamari

  • Status changed from new to infoneeded

Simon, did this ever happen? It looks like most of the tests you list are okay (as of 0499aa7ce68819f72faafdaacda6831ede1ab616),

test status
tc150 ok
tc194 ok
tcfail198 ok
tcfail174 ok
tcfail165 ok
tcfail145 ok
tcfail104 ok
tc211 ok
indexed-types/should_compile/T4120 ok
simpl017 ok
boxy/Base1 broken due to #4295
boxy/Church1 broken due to #4295
boxy/Church2 broken due to #1330
boxy/PList1 broken due to #4295
boxy/PList2 broken due to #4295
boxy/SystemF broken due to #4295
boxy/boxy broken due to #4295
boxy/Compose ok
boxy/T2193 ok
Last edited 6 months ago by bgamari (previous) (diff)

comment:27 Changed 6 months ago by simonpj

No I have not looked at this for ages. Impredicativity is simply not a supported feature at the moment. If things are passing, then let them pass. If you have to change expect_broken to pass, then put a comment in the .hs file to point to this ticket and say that it might be wobbly because of impredicativity.

Simon

comment:28 Changed 3 months ago by thomie

  • Milestone 8.0.1 deleted
Note: See TracTickets for help on using tickets.