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,865
    • Issues 4,865
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 461
    • Merge requests 461
  • 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
  • #19577
Closed
Open
Created Mar 22, 2021 by Sebastian Graf@sgraf812Developer

Type applications in patterns should also work for universal type variables

Consider

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}

module Lib where

import Data.Void

data SMaybe a
  = SNothing
  | SJust !a
  deriving Read

foo :: Read a => (SMaybe a -> r) -> String -> r
foo f s = f (read s)

bar :: _
bar = foo (\(SNothing @Void) -> 42 :: Int) "SNothing"

This compiles and infers bar :: Int on HEAD. Nice!

But it doesn't seem to work in the presence of a type index:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}

module Lib where

data SBool (b :: Bool) where
  STrue :: forall b. (b ~ 'True) => SBool b
  SFalse :: forall b. (b ~ 'False) => SBool b

class Blah b where
  blah :: SBool b

instance Blah 'True where
  blah = STrue

foo :: Blah b => (SBool b -> Int) -> Int
foo f = f blah

bar = foo (\(STrue @True) -> 42)

Error:

test.hs:24:7: error:
    • Ambiguous type variable ‘b0’ arising from a use of ‘foo’
      prevents the constraint ‘(Blah b0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘b0’ should be.
      These potential instance exist:
        instance Blah 'True -- Defined at test.hs:18:10
    • In the expression: foo (\ (STrue @True) -> 42)
      In an equation for ‘bar’: bar = foo (\ (STrue @True) -> 42)
   |
24 | bar = foo (\(STrue @True) -> 42)
   |       ^^^

Here, I expect the specification of @True in the STrue pattern to refine the universal type variable b of the SBool constructor, so that the type of the match is inferred to be SBool 'True. This means I have to write STrue :: SBool 'True.

I believe what happens is that the type variable b of STrue counts as an existential type variable. What a shame. I had hoped that https://dl.acm.org/doi/pdf/10.1145/3242744.3242753 somehow got rid of this distinction.

I feel like I want a bidirectional flow of information (@True informing the match type, the provided constraints of STrue informing any type variables in the match), like unification, instead of just matching the existentially bound var b against the type application in the pattern True and check whether that constraint (b ~ True) is satisfiable.

This was all inspired by https://mail.haskell.org/pipermail/ghc-devs/2021-March/019703.html.

Edited Mar 22, 2021 by Sebastian Graf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking