diff --git a/examples/passing/Proxy.purs b/examples/passing/Proxy.purs
index 1a3984fe50..a2666b37f8 100644
--- a/examples/passing/Proxy.purs
+++ b/examples/passing/Proxy.purs
@@ -18,4 +18,63 @@ i = @"foo"
 j :: Unit
 j = h i
 
+data P t = P
+
+switchP :: forall p. @p -> P p
+switchP _ = P :: P p
+
+switchP' :: forall p. P p -> @p
+switchP' P = @p
+
+type Ap f x = f x
+infix 4 type Ap as $
+type Eg0 = Array $ Unit
+type Eg1 = Array $ Unit
+
+eg0 :: P Eg0
+eg0 = switchP @Eg1
+
+eg0' :: @Eg0
+eg0' = switchP' (P :: P Eg1)
+
+eg1 :: @Eg0
+eg1 = switchP' (switchP @Eg1)
+
+eg1' :: P Eg0
+eg1' = switchP (switchP' (P :: P Eg0))
+
+
+class Go a b | a -> b
+
+instance goInst :: Go Int Int
+
+goGo :: forall a b c. Go a b => Go b c => @a -> P c
+goGo _ = P :: P c
+
+go0 :: P Int
+go0 = goGo @Int
+
+type Go1 = Int
+type Go1' = Int
+
+go1 :: P Go1
+go1 = goGo @Go1'
+
+
+class Determined a p | a -> p where
+  determined :: a -> p
+
+instance determinedIntProxy :: Determined Int @Int where
+  determined _ = @Int
+
+instance determinedProxyInt :: Determined @Int Int where
+  determined _ = 42
+
+determined0 :: @Int
+determined0 = determined 42
+
+determined1 :: Int
+determined1 = determined @Int
+
+
 main = log "Done"
diff --git a/src/Language/PureScript/AST/Traversals.hs b/src/Language/PureScript/AST/Traversals.hs
index 0dce4ae926..54547a87eb 100644
--- a/src/Language/PureScript/AST/Traversals.hs
+++ b/src/Language/PureScript/AST/Traversals.hs
@@ -635,6 +635,7 @@ accumTypes f = everythingOnValues mappend forDecls forValues (const mempty) (con
   forValues (TypeClassDictionary c _ _) = mconcat (fmap f (constraintArgs c))
   forValues (DeferredDictionary _ tys) = mconcat (fmap f tys)
   forValues (TypedValue _ _ ty) = f ty
+  forValues (Proxy ty) = f ty
   forValues _ = mempty
 
 accumKinds
@@ -668,6 +669,7 @@ accumKinds f = everythingOnValues mappend forDecls forValues (const mempty) (con
   forValues (TypeClassDictionary c _ _) = foldMap forTypes (constraintArgs c)
   forValues (DeferredDictionary _ tys) = foldMap forTypes tys
   forValues (TypedValue _ _ ty) = forTypes ty
+  forValues (Proxy ty) = forTypes ty
   forValues _ = mempty
 
   forTypes (KindedType _ k) = f k
@@ -681,5 +683,6 @@ overTypes f = let (_, f', _) = everywhereOnValues id g id in f'
   where
   g :: Expr -> Expr
   g (TypedValue checkTy val t) = TypedValue checkTy val (f t)
+  g (Proxy t) = Proxy (f t)
   g (TypeClassDictionary c sco hints) = TypeClassDictionary (mapConstraintArgs (fmap f) c) sco hints
   g other = other
diff --git a/src/Language/PureScript/Sugar/Names.hs b/src/Language/PureScript/Sugar/Names.hs
index 4afbdccc9e..bfc45f77d4 100644
--- a/src/Language/PureScript/Sugar/Names.hs
+++ b/src/Language/PureScript/Sugar/Names.hs
@@ -269,6 +269,8 @@ renameInModule imports (Module modSS coms mn decls exps) =
     (,) s <$> (Constructor <$> updateDataConstructorName name pos)
   updateValue s@(pos, _) (TypedValue check val ty) =
     (,) s <$> (TypedValue check val <$> updateTypesEverywhere pos ty)
+  updateValue s@(pos, _) (Proxy ty) =
+    (,) s <$> (Proxy <$> updateTypesEverywhere pos ty)
   updateValue s v = return (s, v)
 
   updateBinder
diff --git a/src/Language/PureScript/Sugar/Operators.hs b/src/Language/PureScript/Sugar/Operators.hs
index b537e621a9..8687636e49 100644
--- a/src/Language/PureScript/Sugar/Operators.hs
+++ b/src/Language/PureScript/Sugar/Operators.hs
@@ -356,6 +356,9 @@ updateTypes goType = (goDecl, goExpr, goBinder)
   goExpr pos (TypedValue check v ty) = do
     ty' <- goType' pos ty
     return (pos, TypedValue check v ty')
+  goExpr pos (Proxy ty) = do
+    ty' <- goType' pos ty
+    return (pos, Proxy ty')
   goExpr pos other = return (pos, other)
 
   goBinder :: Maybe SourceSpan -> Binder -> m (Maybe SourceSpan, Binder)
diff --git a/src/Language/PureScript/TypeChecker.hs b/src/Language/PureScript/TypeChecker.hs
index 723db34ff4..3167f81d87 100644
--- a/src/Language/PureScript/TypeChecker.hs
+++ b/src/Language/PureScript/TypeChecker.hs
@@ -199,6 +199,7 @@ checkTypeClassInstance cls i = check where
     TypeApp t1 t2 -> check t1 >> check t2
     REmpty | isFunDepDetermined -> return ()
     RCons _ hd tl | isFunDepDetermined -> check hd >> check tl
+    ProxyType ty -> check ty
     ty -> throwError . errorMessage $ InvalidInstanceHead ty
 
 -- |
diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index 66ba9b2b04..740beb2714 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -496,6 +496,7 @@ matches deps TypeClassDictionaryInScope{..} tys =
     typeHeadsAreEqual t                    (TypeVar v)                     = (Match (), M.singleton v [t])
     typeHeadsAreEqual (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = (Match (), M.empty)
     typeHeadsAreEqual (TypeLevelString s1) (TypeLevelString s2) | s1 == s2 = (Match (), M.empty)
+    typeHeadsAreEqual (ProxyType t1)       (ProxyType t2)                  = typeHeadsAreEqual t1 t2
     typeHeadsAreEqual (TypeApp h1 t1)      (TypeApp h2 t2)                 =
       both (typeHeadsAreEqual h1 h2) (typeHeadsAreEqual t1 t2)
     typeHeadsAreEqual REmpty REmpty = (Match (), M.empty)
@@ -538,6 +539,7 @@ matches deps TypeClassDictionaryInScope{..} tys =
       typesAreEqual (TypeLevelString s1) (TypeLevelString s2) = s1 == s2
       typesAreEqual (TypeConstructor c1) (TypeConstructor c2) = c1 == c2
       typesAreEqual (TypeApp h1 t1)      (TypeApp h2 t2)      = typesAreEqual h1 h2 && typesAreEqual t1 t2
+      typesAreEqual (ProxyType t1)       (ProxyType t2)       = typesAreEqual t1 t2
       typesAreEqual REmpty               REmpty               = True
       typesAreEqual r1                   r2                   | isRCons r1 || isRCons r2 =
           let (common, rest) = alignRowsWith typesAreEqual r1 r2
diff --git a/src/Language/PureScript/TypeChecker/Types.hs b/src/Language/PureScript/TypeChecker/Types.hs
index 05c5bef085..e3bb2d442b 100644
--- a/src/Language/PureScript/TypeChecker/Types.hs
+++ b/src/Language/PureScript/TypeChecker/Types.hs
@@ -394,8 +394,9 @@ infer' (IfThenElse cond th el) = do
 infer' (Let ds val) = do
   (ds', val'@(TypedValue _ _ valTy)) <- inferLetBinding [] ds val infer
   return $ TypedValue True (Let ds' val') valTy
-infer' (Proxy ty) =
-  return $ TypedValue True (Proxy ty) (ProxyType ty)
+infer' (Proxy ty) = do
+  ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
+  return $ TypedValue True (Proxy ty') (ProxyType ty')
 infer' (DeferredDictionary className tys) = do
   dicts <- getTypeClassDictionaries
   hints <- getHints