Support 9.2 with only cmpType changes. #92

philderbeast · 2021-12-31T11:43:53Z

@adamgundry, I noticed that by dropping ghc-9.0 I could get the plugin working with ghc-9.2 by changing only very little, by changing only cmpTyCon, cmpType and cmpTypes.

The quickest way for me to show that this works is to submodule those changes in via ghc-corroborate.

https://github.com/BlockScope/ghc-corroborate/blob/75f90d1d1747395e8017fa16c0a19f5d8a7ad575/ghc-corroborate/src-ghc-9.2/GHC/Corroborate/Compare.hs#L9-L20

All the tests pass with an update to the expected exception strings.

What alerted me to this possibility was working on BlockScope/plugins-for-blobs and seeing the uom-plugin tests failing only in the order of the units, eg. kg m / s versus m kg / s.

I've turned off building the examples for ghc-9.2 as it fails with a core lint error. That's obviously bad but being able to compile the whole of flare-timing against this branch of the uom-plugin with ghc-9.2 without incident is fantastic, see https://github.com/GlideAngle/flare-timing/actions/runs/1640545474. Further good news is this branch doesn't have the convert pack unpack problem.

philderbeast · 2022-01-01T20:12:41Z

I'm getting the same numbers out of flare-timing when I score various comps using this branch of the uom-plugin.

I've added a minimal reproduction of the core lint failure at https://github.com/BlockScope/plugins-for-blobs/tree/repro/example-core-lint.

module UnitDefs (MkUnit) where

import Data.UnitsOfMeasure

[u| m |]
[u| km = 1000m |]

import UnitDefs ()

radiusOfEarth :: Quantity Double [u| km |]
radiusOfEarth = convert [u| 6371000 m |]

main = undefined

If I avoid the conversion then the core lint pass succeeds.

radiusOfEarth :: Quantity Double [u| km |]
-- radiusOfEarth = convert [u| 6371000 m |]
++ radiusOfEarth = [u| 6371 km |]

I found a related issue in GHC 16246 - Non-CoVar has coercion type with an example that passes core linting ghc-8.0.2 through ghc-8.6.3 but then fails with ghc-head as of two years ago.

> cabal build uom-plugin-core-lint
Build profile: -w ghc-9.2.1 -O1
In order, the following will be built (use -v for more details):
 - uom-plugin-core-lint-0.3.0.1 (exe:CoreLintRepro) (first run)
Preprocessing executable 'CoreLintRepro' for uom-plugin-core-lint-0.3.0.1..
Building executable 'CoreLintRepro' for uom-plugin-core-lint-0.3.0.1..
[1 of 2] Compiling UnitDefs
[2 of 2] Compiling Main
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    Non-CoVar has coercion type co_a5PG :: Unpack (Base "m")
                                           ~# ('["m"] ':/ '[])
    Substitution: [TCvSubst
                     In scope: InScope {}
                     Type env: []
                     Co env: []]
*** Offending Program ***
Rec {
$dFractional_a5Nt :: Fractional Double
[LclId]
$dFractional_a5Nt = $fFractionalDouble

$d(%,,%)_a5Ny :: Convertible (Base "m") (Base "km")
[LclId]
$d(%,,%)_a5Ny = ($d(%,,%)_a5Pq, $d(%,,%)_a5Pr, $d~_a5Ps)

$d~_a5Ps :: ToCBU (Unpack (Base "m")) ~ ToCBU (Unpack (Base "km"))
[LclId]
$d~_a5Ps
  = Eq#
      @Unit
      @(ToCBU (Unpack (Base "m")))
      @(ToCBU (Unpack (Base "km")))
      @~(Sym ((((Sym (R:CanonicalBaseUnit"m"[0])
                 *: Sym (D:R:ListToCBU[0]))_N
                ; Sym (D:R:ListToCBU[1] <"m">_N <'[]>_N))
               /: Sym (D:R:ListToCBU[0]))_N
              ; Sym (D:R:ToCBU[0] <'["m"]>_N <'[]>_N)
              ; (ToCBU (Sym co_a5PG))_N)
         ; ((((Sym (D:R:MkUnit"m"[0])
               ; Sym (D:R:CanonicalBaseUnit"km"[0]))
              *: Sym (D:R:ListToCBU[0]))_N
             ; Sym (D:R:ListToCBU[1] <"km">_N <'[]>_N))
            /: Sym (D:R:ListToCBU[0]))_N
         ; Sym (D:R:ToCBU[0] <'["km"]>_N <'[]>_N)
         ; (ToCBU (Sym co_a5PH))_N
         :: ToCBU (Unpack (Base "m")) ~# ToCBU (Unpack (Base "km")))

$d(%,,%)_a5Pq
  :: (Base "m" ~ Pack (Unpack (Base "m")),
      KnownUnit (Unpack (Base "m")), HasCanonical (Unpack (Base "m")))
[LclId]
$d(%,,%)_a5Pq = ($d~_a5Pu, $dKnownUnit_a5Pv, irred_a5Pw)

$d~_a5Pu :: Base "m" ~ Pack (Unpack (Base "m"))
[LclId]
$d~_a5Pu
  = Eq#
      @Unit
      @(Base "m")
      @(Pack (Unpack (Base "m")))
      @~(Sym (Sym ((((<Base "m">_N *: Sym (D:R:Prod[0]))_N
                     ; Sym (D:R:Prod[1] <"m">_N <'[]>_N))
                    /: Sym (D:R:Prod[0]))_N
                   ; Sym (D:R:Pack[0] <'["m"]>_N <'[]>_N)
                   ; (Pack (Sym co_a5PG))_N)
              ; Univ(nominal plugin "units"
                     :: (Base "m" *: One) /: One, Base "m"))
         :: Base "m" ~# Pack (Unpack (Base "m")))

$d(%,,%)_a5Pr
  :: (Base "km" ~ Pack (Unpack (Base "km")),
      KnownUnit (Unpack (Base "km")), HasCanonical (Unpack (Base "km")))
[LclId]
$d(%,,%)_a5Pr = ($d~_a5PB, $dKnownUnit_a5PC, irred_a5PD)

$d~_a5PB :: Base "km" ~ Pack (Unpack (Base "km"))
[LclId]
$d~_a5PB
  = Eq#
      @Unit
      @(Base "km")
      @(Pack (Unpack (Base "km")))
      @~(Sym (Sym ((((<Base "km">_N *: Sym (D:R:Prod[0]))_N
                     ; Sym (D:R:Prod[1] <"km">_N <'[]>_N))
                    /: Sym (D:R:Prod[0]))_N
                   ; Sym (D:R:Pack[0] <'["km"]>_N <'[]>_N)
                   ; (Pack (Sym co_a5PH))_N)
              ; Univ(nominal plugin "units"
                     :: (Base "km" *: One) /: One, Base "km"))
         :: Base "km" ~# Pack (Unpack (Base "km")))

$dNum_a5NU :: Num Double
[LclId]
$dNum_a5NU = $fNumDouble

$dKnownUnit_a5Pv :: KnownUnit (Unpack (Base "m"))
[LclId]
$dKnownUnit_a5Pv
  = $dKnownUnit_a5Qw
    `cast` ((KnownUnit (Sym co_a5PG))_R
            :: KnownUnit ('["m"] ':/ '[]) ~R# KnownUnit (Unpack (Base "m")))

irred_a5Pw :: HasCanonical (Unpack (Base "m"))
[LclId]
irred_a5Pw
  = $d(%,%)_a5Qo
    `cast` (Sub (((%,%)
                    (((%,%)
                        <HasCanonicalBaseUnit "m">_N (Sym (D:R:AllHasCanonical[0])))_N
                     ; Sym (D:R:AllHasCanonical[1] <"m">_N <'[]>_N))
                    (Sym (D:R:AllHasCanonical[0])))_N
                 ; Sym (D:R:HasCanonical[0] <'["m"]>_N <'[]>_N)
                 ; (HasCanonical (Sym co_a5PG))_N)
            :: ((HasCanonicalBaseUnit "m", () :: Constraint), () :: Constraint)
               ~R# HasCanonical (Unpack (Base "m")))

co_a5PG :: Unpack (Base "m") ~# ('["m"] ':/ '[])
[LclId[CoVarId]]
co_a5PG
  = CO: Univ(nominal plugin "units"
             :: Unpack (Base "m"), '["m"] ':/ '[])

$dKnownUnit_a5PC :: KnownUnit (Unpack (Base "km"))
[LclId]
$dKnownUnit_a5PC
  = $dKnownUnit_a5TP
    `cast` ((KnownUnit (Sym co_a5PH))_R
            :: KnownUnit ('["km"] ':/ '[]) ~R# KnownUnit (Unpack (Base "km")))

irred_a5PD :: HasCanonical (Unpack (Base "km"))
[LclId]
irred_a5PD
  = $d(%,%)_a5Qt
    `cast` (Sub (((%,%)
                    (((%,%)
                        <HasCanonicalBaseUnit "km">_N (Sym (D:R:AllHasCanonical[0])))_N
                     ; Sym (D:R:AllHasCanonical[1] <"km">_N <'[]>_N))
                    (Sym (D:R:AllHasCanonical[0])))_N
                 ; Sym (D:R:HasCanonical[0] <'["km"]>_N <'[]>_N)
                 ; (HasCanonical (Sym co_a5PH))_N)
            :: ((HasCanonicalBaseUnit "km", () :: Constraint),
                () :: Constraint)
               ~R# HasCanonical (Unpack (Base "km")))

co_a5PH :: Unpack (Base "km") ~# ('["km"] ':/ '[])
[LclId[CoVarId]]
co_a5PH
  = CO: Univ(nominal plugin "units"
             :: Unpack (Base "km"), '["km"] ':/ '[])

co_a5PI :: Unpack (Base "m") ~# ('["m"] ':/ '[])
[LclId[CoVarId]]
co_a5PI
  = CO: Univ(nominal plugin "units"
             :: Unpack (Base "m"), '["m"] ':/ '[])

co_a5PJ :: Unpack (Base "km") ~# ('["km"] ':/ '[])
[LclId[CoVarId]]
co_a5PJ
  = CO: Univ(nominal plugin "units"
             :: Unpack (Base "km"), '["km"] ':/ '[])

co_a5PK :: Unpack (Base "m") ~# ('["m"] ':/ '[])
[LclId[CoVarId]]
co_a5PK
  = CO: Univ(nominal plugin "units"
             :: Unpack (Base "m"), '["m"] ':/ '[])

co_a5PL :: Unpack (Base "km") ~# ('["km"] ':/ '[])
[LclId[CoVarId]]
co_a5PL
  = CO: Univ(nominal plugin "units"
             :: Unpack (Base "km"), '["km"] ':/ '[])

co_a5PM :: Unpack (Base "m") ~# ('["m"] ':/ '[])
[LclId[CoVarId]]
co_a5PM
  = CO: Univ(nominal plugin "units"
             :: Unpack (Base "m"), '["m"] ':/ '[])

co_a5PN :: Unpack (Base "km") ~# ('["km"] ':/ '[])
[LclId[CoVarId]]
co_a5PN
  = CO: Univ(nominal plugin "units"
             :: Unpack (Base "km"), '["km"] ':/ '[])

co_a5PO :: ('["m"] ':/ '[]) ~# ('["m"] ':/ '[])
[LclId[CoVarId]]
co_a5PO = CO: <'["m"] ':/ '[]>_N

co_a5PP :: Symbol ~# Symbol
[LclId[CoVarId]]
co_a5PP = CO: <Symbol>_N

co_a5PQ :: '["m"] ~# '["m"]
[LclId[CoVarId]]
co_a5PQ = CO: <'["m"]>_N

co_a5PR :: '[] ~# '[]
[LclId[CoVarId]]
co_a5PR = CO: <'[]>_N

co_a5PS :: ('["km"] ':/ '[]) ~# ('["km"] ':/ '[])
[LclId[CoVarId]]
co_a5PS = CO: <'["km"] ':/ '[]>_N

co_a5PT :: Symbol ~# Symbol
[LclId[CoVarId]]
co_a5PT = CO: <Symbol>_N

co_a5PU :: '["km"] ~# '["km"]
[LclId[CoVarId]]
co_a5PU = CO: <'["km"]>_N

co_a5PV :: '[] ~# '[]
[LclId[CoVarId]]
co_a5PV = CO: <'[]>_N

co_a5PW :: ('["m"] ':/ '[]) ~# ('["m"] ':/ '[])
[LclId[CoVarId]]
co_a5PW = CO: <'["m"] ':/ '[]>_N

co_a5PX :: Symbol ~# Symbol
[LclId[CoVarId]]
co_a5PX = CO: <Symbol>_N

co_a5PY :: '["m"] ~# '["m"]
[LclId[CoVarId]]
co_a5PY = CO: <'["m"]>_N

co_a5PZ :: '[] ~# '[]
[LclId[CoVarId]]
co_a5PZ = CO: <'[]>_N

co_a5Q0 :: ('["km"] ':/ '[]) ~# ('["km"] ':/ '[])
[LclId[CoVarId]]
co_a5Q0 = CO: <'["km"] ':/ '[]>_N

co_a5Q1 :: Symbol ~# Symbol
[LclId[CoVarId]]
co_a5Q1 = CO: <Symbol>_N

co_a5Q2 :: '["km"] ~# '["km"]
[LclId[CoVarId]]
co_a5Q2 = CO: <'["km"]>_N

co_a5Q3 :: '[] ~# '[]
[LclId[CoVarId]]
co_a5Q3 = CO: <'[]>_N

co_a5Q4 :: ('["m"] ':/ '[]) ~# ('["m"] ':/ '[])
[LclId[CoVarId]]
co_a5Q4 = CO: <'["m"] ':/ '[]>_N

co_a5Q5 :: Symbol ~# Symbol
[LclId[CoVarId]]
co_a5Q5 = CO: <Symbol>_N

co_a5Q6 :: '["m"] ~# '["m"]
[LclId[CoVarId]]
co_a5Q6 = CO: <'["m"]>_N

co_a5Q7 :: '[] ~# '[]
[LclId[CoVarId]]
co_a5Q7 = CO: <'[]>_N

co_a5Q8 :: ('["km"] ':/ '[]) ~# ('["km"] ':/ '[])
[LclId[CoVarId]]
co_a5Q8 = CO: <'["km"] ':/ '[]>_N

co_a5Q9 :: Symbol ~# Symbol
[LclId[CoVarId]]
co_a5Q9 = CO: <Symbol>_N

co_a5Qa :: '["km"] ~# '["km"]
[LclId[CoVarId]]
co_a5Qa = CO: <'["km"]>_N

co_a5Qb :: '[] ~# '[]
[LclId[CoVarId]]
co_a5Qb = CO: <'[]>_N

$d(%,%)_a5Qo
  :: ((HasCanonicalBaseUnit "m", () :: Constraint), () :: Constraint)
[LclId]
$d(%,%)_a5Qo = ($d(%,%)_a5Qp, $d(%%)_a5Qq)

$d(%,%)_a5Qp :: (HasCanonicalBaseUnit "m", () :: Constraint)
[LclId]
$d(%,%)_a5Qp = ($dHasCanonicalBaseUnit_a5Qr, $d(%%)_a5Qs)

$dHasCanonicalBaseUnit_a5Qr :: HasCanonicalBaseUnit "m"
[LclId]
$dHasCanonicalBaseUnit_a5Qr = $fHasCanonicalBaseUnit"m"

$d(%,%)_a5Qt
  :: ((HasCanonicalBaseUnit "km", () :: Constraint),
      () :: Constraint)
[LclId]
$d(%,%)_a5Qt = ($d(%,%)_a5Qu, $d(%%)_a5Qs)

$d(%,%)_a5Qu :: (HasCanonicalBaseUnit "km", () :: Constraint)
[LclId]
$d(%,%)_a5Qu = ($dHasCanonicalBaseUnit_a5Qv, $d(%%)_a5Qs)

$d(%%)_a5Qq :: () :: Constraint
[LclId]
$d(%%)_a5Qq = $d(%%)_a5Qs

$d(%%)_a5Qs :: () :: Constraint
[LclId]
$d(%%)_a5Qs = (%%)

$dHasCanonicalBaseUnit_a5Qv :: HasCanonicalBaseUnit "km"
[LclId]
$dHasCanonicalBaseUnit_a5Qv = $fHasCanonicalBaseUnit"km"

$dKnownUnit_a5Qw :: KnownUnit ('["m"] ':/ '[])
[LclId]
$dKnownUnit_a5Qw
  = $fKnownUnit:/ @'["m"] @'[] $dKnownList_a5Qz $dKnownList_a5QA

$dKnownList_a5Qz :: KnownList '["m"]
[LclId]
$dKnownList_a5Qz
  = $fKnownList: @"m" @'[] $dKnownSymbol_a5TL $dKnownList_a5TM

$dKnownSymbol_a5TL :: KnownSymbol "m"
[LclId]
$dKnownSymbol_a5TL
  = (unpackCString# "m"#)
    `cast` (Sym (N:KnownSymbol[0] <"m">_N
                 ; N:SSymbol[0] <"m">_P)
            :: String ~R# KnownSymbol "m")

$dKnownUnit_a5TP :: KnownUnit ('["km"] ':/ '[])
[LclId]
$dKnownUnit_a5TP
  = $fKnownUnit:/ @'["km"] @'[] $dKnownList_a5TQ $dKnownList_a5TM

$dKnownList_a5TQ :: KnownList '["km"]
[LclId]
$dKnownList_a5TQ
  = $fKnownList: @"km" @'[] $dKnownSymbol_a5TR $dKnownList_a5TM

$dKnownList_a5QA :: KnownList '[]
[LclId]
$dKnownList_a5QA = $dKnownList_a5TM

$dKnownList_a5TM :: KnownList '[]
[LclId]
$dKnownList_a5TM = $fKnownList[]

$dKnownSymbol_a5TR :: KnownSymbol "km"
[LclId]
$dKnownSymbol_a5TR
  = (unpackCString# "km"#)
    `cast` (Sym (N:KnownSymbol[0] <"km">_N
                 ; N:SSymbol[0] <"km">_P)
            :: String ~R# KnownSymbol "km")

$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Main"#)

main :: forall {a}. a
[LclIdX]
main
  = \ (@a_a5N7) ->
      let {
        $dIP_a5Nh :: ?callStack::CallStack
        [LclId]
        $dIP_a5Nh
          = emptyCallStack
            `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
                    :: CallStack ~R# (?callStack::CallStack)) } in
      let {
        $dIP_a5Nb :: HasCallStack
        [LclId]
        $dIP_a5Nb
          = (pushCallStack
               (unpackCString# "undefined"#,
                SrcLoc
                  (unpackCString# "main"#)
                  (unpackCString# "Main"#)
                  (unpackCString# "CoreLintRepro.hs"#)
                  (I# 17#)
                  (I# 8#)
                  (I# 17#)
                  (I# 17#))
               ($dIP_a5Nh
                `cast` (N:IP[0] <"callStack">_N <CallStack>_N
                        :: (?callStack::CallStack) ~R# CallStack)))
            `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
                    :: CallStack ~R# (?callStack::CallStack)) } in
      letrec {
        main_a5Nc :: a_a5N7
        [LclId]
        main_a5Nc = undefined @('BoxedRep 'Lifted) @a_a5N7 $dIP_a5Nb; } in
      main_a5Nc

radiusOfEarth :: Quantity Double (MkUnit "km")
[LclId]
radiusOfEarth
  = (convert
       @Double
       @(Base "m")
       @(Base "km")
       $dFractional_a5Nt
       $d(%,,%)_a5Ny
       (((\ (@a_a5NL) ->
            ((\ (@a_a5qj) (@(u_a5qk :: Unit)) (ds_d5V9 :: a_a5qj) ->
                MkQuantity @a_a5qj @u_a5qk ds_d5V9)
               @a_a5NL @(Base "m"))
            `cast` (<a_a5NL>_R
                    %<'Many>_N ->_R (Quantity <a_a5NL>_R (Sym (D:R:MkUnit"m"[0])))_R
                    :: (a_a5NL -> Quantity a_a5NL (Base "m"))
                       ~R# (a_a5NL -> Quantity a_a5NL (MkUnit "m"))))
           @Double (D# 6371000.0##))
        `cast` ((Quantity <Double>_R (D:R:MkUnit"m"[0]))_R
                :: Quantity Double (MkUnit "m") ~R# Quantity Double (Base "m"))))
    `cast` ((Quantity <Double>_R (Sym (D:R:MkUnit"km"[0])))_R
            :: Quantity Double (Base "km") ~R# Quantity Double (MkUnit "km"))

main :: IO Any
[LclIdX]
main = runMainIO @Any (main @(IO Any))
end Rec }

*** End of Offense ***


<no location info>: error:
Compilation had errors

philderbeast · 2022-03-12T11:22:16Z

I've published ghc-corroborate so we can remove it as a git submodule.

philderbeast added 11 commits December 29, 2021 16:02

Redo *.cabal file generation and *.dhall formatting.

9b684ee

Follow hlint suggestions.

1c575f6

Drop dhall depenedency from build.

1845e08

Drop uom-plugin:hlint test suite.

b7b2954

Add github action for build and test with cabal.

ac9c4f8

Missed removing some hlint stale directories.

0e66ddd

Build uom-plugin:units with ghc-9.2 using ghc-corroborate.

ccd554a

Merge test exception expectations by ghc version.

7bd3b2a

Add uom-plugin-defs, merge tricks for uom-plugin-tutorial.

1b36e6a

For ghc-9.2.1 use src-ghc-9.0 folder for doctest.

08ce032

Fix StarIsType warning.

8b22e63

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support 9.2 with only cmpType changes. #92

Support 9.2 with only cmpType changes. #92

philderbeast commented Dec 31, 2021

philderbeast commented Jan 1, 2022 •

edited

Loading

philderbeast commented Mar 12, 2022

Support 9.2 with only cmpType changes. #92

Are you sure you want to change the base?

Support 9.2 with only cmpType changes. #92

Conversation

philderbeast commented Dec 31, 2021

philderbeast commented Jan 1, 2022 • edited Loading

philderbeast commented Mar 12, 2022

philderbeast commented Jan 1, 2022 •

edited

Loading