Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Register
  • Sign in
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
    • Locked files
  • Issues 5.5k
    • Issues 5.5k
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 624
    • Merge requests 624
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
    • Test cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • 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 CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #23333
Closed
Open
Issue created May 02, 2023 by Mikolaj Konarski@MikolajReporter

Swapping arguments of type comparison operator ~ induces a type error

Summary

Edit2: see later comments for an even smaller repro.

Edit: a minimal repro is at https://play.haskell.org/saved/EtiAllWh (uncomment the bit swapping ~ arguments to make it fail)

The following commit, swapping arguments of an application of the type comparison operator ~ induces, a type error. No plugins are used in this file.

https://github.com/Mikolaj/horde-ad/commit/3905cf0515ce5ce2723b4b0140184e4c8dcc9599

Steps to reproduce

Compile with and without this commit, using cabal build -j1 (for GHC 9.6 add --allow-newer). It should compile fine without the commit and with it it should fail emitting

simplified/HordeAd/Core/AstInterpret.hs:200:16: error: [GHC-05617]
    • Could not deduce ‘BooleanOf (Ranked (Primal a) n)
                        ~ BooleanOf (IntOf a)’
      from the context: InterpretAst a
        bound by the type signature for:
                   interpretAstBool :: forall a.
                                       InterpretAst a =>
                                       AstEnv a
                                       -> AstMemo a
                                       -> AstBool (ScalarOf a)
                                       -> (AstMemo a, BooleanOf (Primal a))
        at simplified/HordeAd/Core/AstInterpret.hs:(190,1)-(192,77)
      Expected: BooleanOf (Primal a)
        Actual: BooleanOf (Ranked (Primal a) n)
        NB: ‘BooleanOf’ is a non-injective type family
    • In the expression: interpretAstRelOp opCodeRel args2
      In the expression: (memo2, interpretAstRelOp opCodeRel args2)
      In the expression:
        let (memo2, args2) = mapAccumR (interpretAstPrimal env) memo args
        in (memo2, interpretAstRelOp opCodeRel args2)
    • Relevant bindings include
        memo2 :: AstMemo a
          (bound at simplified/HordeAd/Core/AstInterpret.hs:199:10)
        args2 :: [Ranked (Primal a) n]
          (bound at simplified/HordeAd/Core/AstInterpret.hs:199:17)
        args :: [AstPrimalPart n (ScalarOf a)]
          (bound at simplified/HordeAd/Core/AstInterpret.hs:198:20)
        memo :: AstMemo a
          (bound at simplified/HordeAd/Core/AstInterpret.hs:193:22)
        env :: AstEnv a
          (bound at simplified/HordeAd/Core/AstInterpret.hs:193:18)
        interpretAstBool :: AstEnv a
                            -> AstMemo a
                            -> AstBool (ScalarOf a)
                            -> (AstMemo a, BooleanOf (Primal a))
          (bound at simplified/HordeAd/Core/AstInterpret.hs:193:1)
    |
200 |     in (memo2, interpretAstRelOp opCodeRel args2)

Expected behavior

Compiles both with and without the commit.

Environment

  • GHC version used: 9.4.5 and 9.6.1

BTW, a different version of this code, one that does not require QuantifiedConstraints and has foralls in a very different place, is similarly fragile (flip argumenta in both BooleanOf (IntOf a) ~ BooleanOf (Ranked (Primal a) n) to make it fail): https://github.com/Mikolaj/horde-ad/blob/f40c4706657b80e8326468bb299456d319cce325/simplified/HordeAd/Core/AstInterpret.hs#L102-L122

Edited May 02, 2023 by Mikolaj Konarski
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking