Solve u ~ Pack (Unpack u) in plugin

[adamgundry]

See #23.

[expipiplus1]

This seems to be the cause of a regression since ghc-7.10.3

This compiles without issue with 7.10.3 but fails to compile with ghc-8.0.1

{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}
{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}

module Bug where

import Data.UnitsOfMeasure.Defs     ()
import Data.UnitsOfMeasure

foo :: forall a. Fractional a => Quantity a [u|s|]
foo = convert $ bar b
  where
    b :: Quantity a [u|s * s|]
    b = b

bar :: Quantity a (u*:u) -> Quantity a u
bar = bar

[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:12:7: error:
    • Occurs check: cannot construct the infinite type:
        t0 ~ Unpack (Pack t0)
        arising from a use of ‘convert’
      The type variable ‘t0’ is ambiguous
    • In the expression: convert $ bar b
      In an equation for ‘foo’:
          foo
            = convert $ bar b
            where
                b :: Quantity a ((*:) (MkUnit "s") (MkUnit "s"))
                b = b

Bug.hs:12:7: error:
    • Couldn't match type ‘Data.UnitsOfMeasure.Convert.ToCBU t0’
                     with ‘(Base "s" *: One) /: One’
        arising from a use of ‘convert’
      The type variable ‘t0’ is ambiguous
    • In the expression: convert $ bar b
      In an equation for ‘foo’:
          foo
            = convert $ bar b
            where
                b :: Quantity a ((*:) (MkUnit "s") (MkUnit "s"))
                b = b

Bug.hs:12:21: error:
    • Couldn't match type ‘Base "s" *: Base "s"’
                     with ‘Pack t0 *: Pack t0’
      Expected type: Quantity a (Pack t0 *: Pack t0)
        Actual type: Quantity a (MkUnit "s" *: MkUnit "s")
      NB: ‘*:’ is a type function, and may not be injective
      The type variable ‘t0’ is ambiguous
    • In the first argument of ‘bar’, namely ‘b’
      In the second argument of ‘($)’, namely ‘bar b’
      In the expression: convert $ bar b

[adamgundry]

Thanks for reporting this. The problem seems to be the failure to solve for t0, but I need to dig further to work out where it is being introduced. That occurs check failure is wrong, so there may be a GHC bug involved here.

[expipiplus1]

So could it be that GHC is failing on the spurious occurs check before uom-plugin gets a chance to solve things?

[adamgundry]

Perhaps. I don't know whether GHC is failing too early because of the occurs check, or whether it is simply misreporting an unsolved constraint error as an occurs check failure.