src/Core/HindleyMilner.hs

@@ -7,6 +7,7 @@ module Core.HindleyMilner
     ( infer
     , Context'
     , TypeError(..)
+    , HMError
     )
     where
 ----------------------------------------------------------------------------------
@@ -50,7 +51,7 @@ type HMError = Either TypeError
 -- >>> infer g2 [coreExpr|id 3|]
 -- Left (TyErrCouldNotUnify (TyVar "a" :-> TyVar "a") TyInt)
 
-infer :: Context' -> Expr' -> Either TypeError Type
+infer :: Context' -> Expr' -> HMError Type
 infer g e = do
     (t,cs) <- gather g e
     foldr (uncurry subst) t <$> unify cs

src/Core/Syntax.hs

@@ -126,6 +126,9 @@ type Binding' = Binding Name
 instance IsString (Expr b) where
     fromString = Var
 
+instance IsString Type where
+    fromString = TyVar
+
 instance Semigroup (Program b) where
     (<>) = coerce $ (<>) @[ScDef b] 
 

tst/Core/HindleyMilnerSpec.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE QuasiQuotes, OverloadedStrings #-}
 module Core.HindleyMilnerSpec
     ( spec
     )
@@ -6,7 +6,7 @@ module Core.HindleyMilnerSpec
 ----------------------------------------------------------------------------------
 import Core.Syntax
 import Core.TH                  (coreExpr)
-import Core.HindleyMilner       (infer)
+import Core.HindleyMilner       (infer, TypeError(..), HMError)
 import Test.Hspec
 ----------------------------------------------------------------------------------
 
@@ -14,6 +14,14 @@ import Test.Hspec
 spec :: Spec
 spec = do
     it "should infer `id 3` :: Int" $
-        let g = [ ("id", TyVar "a" :-> TyVar "a") ]
+        let g = [ ("id", "a" :-> "a") ]
         in infer g [coreExpr|id 3|] `shouldBe` Right TyInt
 
+    it "should not infer `id 3` when `id` is specialised to `a -> a`" $
+        let g = [ ("id", ("a" :-> "a") :-> "a" :-> "a") ]
+        in infer g [coreExpr|id 3|] `shouldSatisfy` isUntypedVariableErr
+
+isUntypedVariableErr :: HMError a -> Bool
+isUntypedVariableErr (Left (TyErrCouldNotUnify _ _)) = True
+isUntypedVariableErr _                               = False
+