nikita-volkov / refined

Refinement types with static checking
http://hackage.haskell.org/package/refined
MIT License
183 stars 31 forks source link

Type inference of the refineTH splice doesn't work with a newtype wrapper. #79

Closed Goheeca closed 2 years ago

Goheeca commented 3 years ago

When I created a newtype of the refined type, type inference no longer works and I have to resort to type application. I'm not sure if whether it's limitation of TH alone or not. Here's the code demonstrating the issue:

RefinedTestDefinitions.hs

{-# LANGUAGE DeriveLift, MultiParamTypeClasses #-}
module RefinedTestDefinitions (
  UnrefinedTest(..),
  RefinedTest,
  WrappedRefinedTest(..),
) where

import Refined
import Language.Haskell.TH.Syntax

data UnrefinedTest a = UnrefinedTest a deriving Lift

data TestValidator
instance Predicate TestValidator (UnrefinedTest a) where
  validate _ _ = Nothing

type RefinedTest a = Refined TestValidator (UnrefinedTest a)
newtype WrappedRefinedTest a = WrappedRefinedTest (RefinedTest a)

RefinedTest.hs

#!/usr/bin/env stack
-- stack --resolver lts-18.5 script --package template-haskell --package refined
{-# LANGUAGE TemplateHaskell, TypeApplications #-}

import Refined
import Data.Either

import RefinedTestDefinitions

refinedTypeAppliedTest :: RefinedTest Int
refinedTypeAppliedTest = $$(refineTH $ UnrefinedTest @Int 0)

refinedTest :: RefinedTest Int
refinedTest = $$(refineTH $ UnrefinedTest 0)

wrappedRefinedTypeAppliedTest :: WrappedRefinedTest Int
wrappedRefinedTypeAppliedTest = WrappedRefinedTest $ fromRight undefined $ refine $ UnrefinedTest @Int 0

wrappedRefinedTest :: WrappedRefinedTest Int
wrappedRefinedTest = WrappedRefinedTest $ fromRight undefined $ refine $ UnrefinedTest 0

wrappedRefinedTypeAppliedTHTest :: WrappedRefinedTest Int
wrappedRefinedTypeAppliedTHTest = WrappedRefinedTest $$(refineTH $ UnrefinedTest @Int 0)

{- The following fails because:
    • Ambiguous type variable ‘a0’ arising from a use of ‘refineTH’
      prevents the constraint ‘(Language.Haskell.TH.Syntax.Lift
                                  a0)’ from being solved.
    • Ambiguous type variable ‘a0’ arising from the literal ‘0’
      prevents the constraint ‘(Num a0)’ from being solved.
-}
wrappedRefinedTHTest :: WrappedRefinedTest Int
wrappedRefinedTHTest = WrappedRefinedTest $$(refineTH $ UnrefinedTest 0)

main = pure ()

I also prepared a gist for easier downloading.

chessai commented 2 years ago

Yeah, there's nothing I can do about this, unfortunately. You need to provide a type.

blamario commented 2 years ago

I've run into the same problem. Is there a GHC issue opened about this?